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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-08-06 08:16:50 -04:00
parent 73e67b8d3d
commit 9123431424
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean
View file

@ -53,7 +53,8 @@ instance : IndexNotation (realLorentzTensor d).Color := instIndexNotationColorRe
instance : DecidableEq (realLorentzTensor d).Color := instDecidableEqColorRealTensorColor
@[simp]
lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d = instIndexNotationColorRealTensorColor := by
lemma indexNotation_eq_color : @realLorentzTensor.instIndexNotationColor d =
instIndexNotationColorRealTensorColor := by
rfl
@[simp]
@ -76,7 +77,8 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color}
(hs : listCharIndexStringBool realTensorColor.Color s.toList = true)
(hn : n = (IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)).length)
(hc : IndexListColor.colorPropBool (IndexString.toIndexList ⟨s, hs⟩))
(hd : TensorColor.DualMap.boolFin (IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
(hd : TensorColor.DualMap.boolFin
(IndexString.toIndexList ⟨s, hs⟩).colorMap (cn ∘ Fin.cast hn.symm)) :
(realLorentzTensor d).TensorIndex :=
TensorStructure.TensorIndex.mkDualMap T
⟨(IndexString.toIndexList (⟨s, hs⟩ : IndexString realTensorColor.Color)),