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-06-13 10:59:10 -04:00
parent de89fd7ef0
commit f50b2547c7
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean.lean
View file

@ -68,6 +68,7 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous
import HepLean.SpaceTime.LorentzGroup.Proper
import HepLean.SpaceTime.LorentzGroup.Rotations
import HepLean.SpaceTime.Metric
import HepLean.SpaceTime.SL2C.Basic
import HepLean.StandardModel.Basic
import HepLean.StandardModel.HiggsBoson.Basic
import HepLean.StandardModel.HiggsBoson.TargetSpace

2
HepLean/AnomalyCancellation/SM/Basic.lean
View file

@ -52,7 +52,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMCharges n).charges) :
exact fun a i => congrArg (⇑(toSpecies i)) a
intro h
apply toSpeciesEquiv.injective
exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ a => h x
exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ _ => h x
lemma toSMSpecies_toSpecies_inv (i : Fin 5) (f : (Fin 5 → Fin n → ℚ) ) :
(toSpecies i) (toSpeciesEquiv.symm f) = f i := by