DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore: Replace Finset.sum_product

Browse source
This commit is contained in:
jstoobysmith 2025-03-24 09:14:57 -04:00
parent c6d65bb308
commit d18ede024d
5 changed files with 38 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

2
PhysLean/Relativity/Lorentz/ComplexTensor/OfRat.lean
View file

@ -145,7 +145,7 @@ lemma contr_ofRat {n : ℕ} {c : Fin (n + 1 + 1) → complexLorentzTensor.C} {i
congr
funext b
rw [← (contrSectionEquiv b).symm.sum_comp]
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
congr
funext x
rw [Finset.sum_eq_single (Fin.cast (by simp [h]) x)]

16
PhysLean/Relativity/Lorentz/ComplexVector/Two.lean
View file

@ -33,7 +33,7 @@ lemma contrContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1
simp only [Action.instMonoidalCategory_tensorObj_V, contrContrToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply complexContrBasis complexContrBasis i j]
rfl
@ -52,7 +52,7 @@ lemma coCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin
simp only [Action.instMonoidalCategory_tensorObj_V, coCoToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply complexCoBasis complexCoBasis i j]
rfl
@ -71,7 +71,7 @@ lemma contrCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕
simp only [Action.instMonoidalCategory_tensorObj_V, contrCoToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply complexContrBasis complexCoBasis i j]
rfl
@ -90,7 +90,7 @@ lemma coContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕
simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply complexCoBasis complexContrBasis i j]
rfl
@ -126,7 +126,7 @@ lemma contrContrToMatrix_ρ (v : (complexContr ⊗ complexContr).V) (M : SL(2,
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
* contrContrToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
contrContrToMatrix v x1 x) * LorentzGroup.toComplex (SL2C.toLorentzGroup M) j x
@ -168,7 +168,7 @@ lemma coCoToMatrix_ρ (v : (complexCo ⊗ complexCo).V) (M : SL(2,ℂ)) :
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
* coCoToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
coCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
@ -210,7 +210,7 @@ lemma contrCoToMatrix_ρ (v : (complexContr ⊗ complexCo).V) (M : SL(2,ℂ)) :
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M))
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M)) (i, j) k)
* contrCoToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
have h1 : ∑ x, (∑ x1, LorentzGroup.toComplex (SL2C.toLorentzGroup M) i x1 *
contrCoToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x j
@ -253,7 +253,7 @@ lemma coContrToMatrix_ρ (v : (complexCo ⊗ complexContr).V) (M : SL(2,ℂ)) :
((LinearMap.toMatrix complexCoBasis complexCoBasis) (complexCo.ρ M))
((LinearMap.toMatrix complexContrBasis complexContrBasis) (complexContr.ρ M)) (i, j) k)
* coContrToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x, (∑ x1, (LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ x1 i *
coContrToMatrix v x1 x) * (LorentzGroup.toComplex (SL2C.toLorentzGroup M)) j x

2
PhysLean/Relativity/Lorentz/RealTensor/Basic.lean
View file

@ -242,7 +242,7 @@ lemma contr_tensorBasis_repr_apply_eq_fin {n d: ℕ} {c : Fin (n + 1 + 1) → (r
(liftToContrSection b ⟨Fin.cast (by simp) x, Fin.cast (by simp) x⟩)) := by
rw [contr_tensorBasis_repr_apply_eq_contrSection]
rw [← (contrSectionEquiv b).symm.sum_comp]
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
let e : Fin ((realLorentzTensor d).repDim (c i)) ≃ Fin (1 + d) :=
(Fin.castOrderIso (by simp)).toEquiv
rw [← e.symm.sum_comp]

16
PhysLean/Relativity/Lorentz/RealTensor/Matrix/Pre.lean
View file

@ -32,7 +32,7 @@ lemma contrContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
simp only [contrContrToMatrixRe, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply (contrBasis d) (contrBasis d) i j]
rfl
@ -51,7 +51,7 @@ lemma coCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ F
simp only [Action.instMonoidalCategory_tensorObj_V, coCoToMatrixRe, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply (coBasis d) (coBasis d) i j]
rfl
@ -70,7 +70,7 @@ lemma contrCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
simp only [contrCoToMatrixRe, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply _ _ i j]
rfl
@ -89,7 +89,7 @@ lemma coContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
simp only [Action.instMonoidalCategory_tensorObj_V, coContrToMatrixRe, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℝ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply _ _ i j]
rfl
@ -124,7 +124,7 @@ lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : Loren
((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
* contrContrToMatrixRe v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
conv_rhs =>
enter [2, x]
@ -160,7 +160,7 @@ lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup
((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
* coCoToMatrixRe v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
conv_rhs =>
enter [2, x]
@ -197,7 +197,7 @@ lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : Lorentz
((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
* contrCoToMatrixRe v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
conv_rhs =>
enter [2, x]
@ -234,7 +234,7 @@ lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : Lorentz
((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
* coContrToMatrixRe v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
conv_rhs =>
enter [2, x]

40
PhysLean/Relativity/Lorentz/Weyl/Two.lean
View file

@ -38,7 +38,7 @@ lemma leftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, leftLeftToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply leftBasis leftBasis i j]
rfl
@ -56,7 +56,7 @@ lemma altLeftaltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, altLeftaltLeftToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply altLeftBasis altLeftBasis i j]
rfl
@ -74,7 +74,7 @@ lemma leftAltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply leftBasis altLeftBasis i j]
rfl
@ -92,7 +92,7 @@ lemma altLeftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply altLeftBasis leftBasis i j]
rfl
@ -110,7 +110,7 @@ lemma rightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, rightRightToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply rightBasis rightBasis i j]
rfl
@ -129,7 +129,7 @@ lemma altRightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ)
simp only [Action.instMonoidalCategory_tensorObj_V, altRightAltRightToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply altRightBasis altRightBasis i j]
rfl
@ -147,7 +147,7 @@ lemma rightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply rightBasis altRightBasis i j]
rfl
@ -165,7 +165,7 @@ lemma altRightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply altRightBasis rightBasis i j]
rfl
@ -183,7 +183,7 @@ lemma altLeftAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ)
simp only [Action.instMonoidalCategory_tensorObj_V, altLeftAltRightToMatrix,
LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply altLeftBasis altRightBasis i j]
rfl
@ -201,7 +201,7 @@ lemma leftRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
simp only [Action.instMonoidalCategory_tensorObj_V, leftRightToMatrix, LinearEquiv.trans_symm,
LinearEquiv.trans_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
· erw [Finset.sum_product]
· rw [Fintype.sum_prod_type]
refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
erw [Basis.tensorProduct_apply leftBasis rightBasis i j]
rfl
@ -236,7 +236,7 @@ lemma leftLeftToMatrix_ρ (v : (leftHanded ⊗ leftHanded).V) (M : SL(2,ℂ)) :
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
* leftLeftToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ j : Fin 2, M.1 i j * leftLeftToMatrix v j x) * M.1 j x
= ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftLeftToMatrix v x1 x) * M.1 j x := by
@ -279,7 +279,7 @@ lemma altLeftaltLeftToMatrix_ρ (v : (altLeftHanded ⊗ altLeftHanded).V) (M : S
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
* altLeftaltLeftToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j
= ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j := by
@ -319,7 +319,7 @@ lemma leftAltLeftToMatrix_ρ (v : (leftHanded ⊗ altLeftHanded).V) (M : SL(2,
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
* leftAltLeftToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j
= ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j := by
@ -360,7 +360,7 @@ lemma altLeftLeftToMatrix_ρ (v : (altLeftHanded ⊗ leftHanded).V) (M : SL(2,
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
* altLeftLeftToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x
= ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x:= by
@ -401,7 +401,7 @@ lemma rightRightToMatrix_ρ (v : (rightHanded ⊗ rightHanded).V) (M : SL(2,ℂ)
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
* rightRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightRightToMatrix v x1 x) *
(M.1.map star) j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@ -443,7 +443,7 @@ lemma altRightAltRightToMatrix_ρ (v : (altRightHanded ⊗ altRightHanded).V) (M
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
* altRightAltRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (↑M)⁻¹ᴴ i x1 * altRightAltRightToMatrix v x1 x) *
(↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@ -484,7 +484,7 @@ lemma rightAltRightToMatrix_ρ (v : (rightHanded ⊗ altRightHanded).V) (M : SL(
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
* rightAltRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightAltRightToMatrix v x1 x)
* (↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@ -526,7 +526,7 @@ lemma altRightRightToMatrix_ρ (v : (altRightHanded ⊗ rightHanded).V) (M : SL(
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
* altRightRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2,
(↑M)⁻¹ᴴ i x1 * altRightRightToMatrix v x1 x) * (M.1.map star) j x
@ -567,7 +567,7 @@ lemma altLeftAltRightToMatrix_ρ (v : (altLeftHanded ⊗ altRightHanded).V) (M :
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
* altLeftAltRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftAltRightToMatrix v x1 x) *
(M.1)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
@ -607,7 +607,7 @@ lemma leftRightToMatrix_ρ (v : (leftHanded ⊗ rightHanded).V) (M : SL(2,ℂ))
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
* leftRightToMatrix v k.1 k.2) = _
erw [Finset.sum_product]
rw [Fintype.sum_prod_type]
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j
= ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftRightToMatrix v x1 x) * (M.1)ᴴ x j := by