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-26 06:00:22 -04:00
parent 6d81fc2fd8
commit d56444a0c1
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
View file

@ -415,6 +415,7 @@ end append
-/
/-- The number of times the id of an index `I` appears in a list of indices `l`. -/
def countId (I : Index X) : ℕ :=
l.val.countP (fun J => I.id = J.id)

2
HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean
View file

@ -211,7 +211,7 @@ lemma iff_countP_isSome (hl : l.withUniqueDual = l.withDual) :
· exact hi1.symm
lemma iff_countP (hl : l.withUniqueDual = l.withDual) :
l.ColorCond ↔ ∀ (i : Fin l.length), l.countId (l.val.get i) = 2
l.ColorCond ↔ ∀ (i : Fin l.length), l.countId (l.val.get i) = 2
→ countPCond l (l.val.get i) := by
rw [iff_countP_isSome hl]
refine Iff.intro (fun h i hi => ?_) (fun h i hi => ?_)