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

docs: Missing comma

Browse source
This commit is contained in:
jstoobysmith 2024-07-16 11:43:59 -04:00
parent 9c77e18a70
commit 86e7ea6c0f
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
View file

@ -21,7 +21,7 @@ open SMνCharges
open SMνACCs
open BigOperators
/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
/-- A proposition which is true if for a given `n`, a plane of charges of dimension `n` exists
in which each point is a solution. -/
def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges),
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)