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

Update Parameterization.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-21 14:10:56 +02:00
parent 720afc70e8
commit 87183d6e93
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
View file

@ -16,7 +16,7 @@ import Mathlib.Tactic.Polyrith
Given maps `g : Fin n.succ → ℚ`, `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
equations. We show that every solution can be got in this way, up to permutation, unless it, up to
permutaiton, lives in the plane spanned by the firt part of the basis vector.
permutation, lives in the plane spanned by the first part of the basis vector.
The main reference is:
@ -32,7 +32,7 @@ open BigOperators
variable {n : ℕ}
open VectorLikeEvenPlane
/-- Given coefficents `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
/-- Given coefficients `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
rational `a ∈ ℚ`, we get a
point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show extends to an anomaly
free point. -/