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

feat: tensorindex rel of withDual empty

Browse source
This commit is contained in:
jstoobysmith 2024-08-19 09:23:57 -04:00
parent e15aaadcb6
commit b67a7dbb7f
4 changed files with 110 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Lemmas.lean
View file

@ -17,16 +17,23 @@ open IndexNotation IndexString
open TensorStructure TensorIndex
variable {R : Type} [CommSemiring R] {n m : ℕ}
/-lemma swap_eq_transpose (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) :
/-
lemma swap_eq_transpose (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) :
(T|"ᵢ₁ᵢ₂") ≈ ((toMatrix.symm (toMatrix T).transpose)|"ᵢ₂ᵢ₁") := by
apply And.intro
refine Rel.of_withDual_empty ?_ ?_ ?_ ?_
· apply And.intro
simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr, fromIndexStringColor,
mkDualMap, decidableEq_eq_color]
decide
simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr, fromIndexStringColor,
mkDualMap, decidableEq_eq_color, ColorIndexList.colorMap']
simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
ColorIndexList.colorMap', decidableEq_eq_color, ColorIndexList.contr]
decide
intro h -/
· simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
decidableEq_eq_color]
decide
· simp only [toTensorColor_eq, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
ColorIndexList.colorMap', decidableEq_eq_color]
decide
simp [fromIndexStringColor, mkDualMap]-/
end einsteinTensor