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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-04-18 11:44:06 -04:00
parent e6f12ddae6
commit 154de6ad9e
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -32,12 +32,12 @@ open VectorLikeOddPlane
/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a linear solution. We will later
show that this can be extended to a complete solution. -/
def parameterizationAsLinear (g f : Fin n → ℚ) (a : ℚ) :
(PureU1 (2 * n + 1)).LinSols :=
(PureU1 (2 * n + 1)).LinSols :=
a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
(- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
(parameterizationAsLinear g f a).val =
(parameterizationAsLinear g f a).val =
a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
(- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
rw [parameterizationAsLinear]
@ -118,7 +118,7 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : genericCase S) :
∃ g f a, S = parameterization g f a := by
∃ g f a, S = parameterization g f a := by
obtain ⟨g, f, hS⟩ := span_basis S.1.1
use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
rw [parameterization]