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

Update LinearParameterization.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-21 14:12:53 +02:00
parent 87183d6e93
commit 4528d22dc6
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
View file

@ -46,7 +46,7 @@ lemma ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E
cases' S
simp_all only
/-- The map from the linear paramaters to elements of `(SMNoGrav 1).charges`. -/
/-- The map from the linear parameters to elements of `(SMNoGrav 1).charges`. -/
@[simp]
def asCharges (S : linearParameters) : (SMNoGrav 1).charges := fun i =>
match i with