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-11-22 15:37:01 +00:00
parent be64dbb8bb
commit 49acdc18b2
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/FeynmanDiagrams/Wick/Contract.lean
View file

@ -359,7 +359,7 @@ def Level {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) (k : ℕ) :
Σ (b1 : Fin k → Fin n) (b2 : Fin k → Fin n), WickContract str b1 b2
/-- There is a finite number of Wick contractions with no contractions. In particular,
this is just the original Wick string. -/
this is just the original Wick string. -/
instance levelZeroFintype {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) :
Fintype (Level str 0) where
elems := {⟨Fin.elim0, Fin.elim0, WickContract.string⟩}