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:28 +02:00
parent c768e660a1
commit a368679152
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -13,7 +13,7 @@ import Mathlib.Logic.Equiv.Fin
/-!
# Anomaly cancellation conditions for n family SM.
We define the ACC system for the Standard Model with`n`-famlies and no RHN.
We define the ACC system for the Standard Model with`n`-families and no RHN.
-/
@ -21,7 +21,7 @@ universe v u
open Nat
open BigOperators
/-- Aassociate to each (including RHN) SM fermion a set of charges-/
/-- Associate to each (including RHN) SM fermion a set of charges-/
@[simps!]
def SMCharges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk (5 * n)