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

Update Basic.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-20 00:19:16 +02:00
parent 2195936a88
commit 718b1049d1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -206,7 +206,7 @@ lemma accSU2_ext {S T : MSSMCharges.charges}
rw [hd, hu]
rfl
/-- The anomaly cancelation condition for SU(3) anomaly. -/
/-- The anomaly cancellation condition for SU(3) anomaly. -/
@[simp]
def accSU3 : MSSMCharges.charges →ₗ[ℚ] ℚ where
toFun S := ∑ i, (2 * (Q S i) + (U S i) + (D S i))