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:15 +02:00
parent 926653a049
commit 2195936a88
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/Basic.lean
View file

@ -77,7 +77,7 @@ namespace ACCSystemLinear
structure LinSols (χ : ACCSystemLinear) where
/-- The underlying charge. -/
val : χ.1.charges
/-- The condition that the charge satifies the linear ACCs. -/
/-- The condition that the charge satisfies the linear ACCs. -/
linearSol : ∀ i : Fin χ.numberLinear, χ.linearACCs i val = 0
/-- Two solutions are equal if the underlying charges are equal. -/
@ -172,7 +172,7 @@ namespace ACCSystemQuad
/-- The type of solutions to the linear and quadratic ACCs. -/
structure QuadSols (χ : ACCSystemQuad) extends χ.LinSols where
/-- The condition that the charge satifies the quadratic ACCs. -/
/-- The condition that the charge satisfies the quadratic ACCs. -/
quadSol : ∀ i : Fin χ.numberQuadratic, (χ.quadraticACCs i) val = 0
/-- Two `QuadSols` are equal if the underlying charges are equal. -/
@ -225,7 +225,7 @@ namespace ACCSystem
/-- The type of solutions to the anomaly cancellation conditions. -/
structure Sols (χ : ACCSystem) extends χ.QuadSols where
/-- The condition that the charge satifies the cubic ACC. -/
/-- The condition that the charge satisfies the cubic ACC. -/
cubicSol : χ.cubicACC val = 0
/-- Two solutions are equal if the underlying charges are equal. -/