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-08-21 06:45:09 -04:00
parent c0499483a8
commit c2eb4bbe9d
8 changed files with 11 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
View file

@ -37,7 +37,6 @@ lemma constAbs_perm (S : (PureU1 n).Charges) (M :(FamilyPermutations n).group) :
simp at h2
exact h2
lemma constAbs_sort {S : (PureU1 n).Charges} (CA : ConstAbs S) : ConstAbs (sort S) := by
rw [sort]
exact (constAbs_perm S _).mpr CA

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

@ -153,7 +153,7 @@ lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
SpecialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) :
LineInCubicPerm S.1.1 :=
fun M => special_case_lineInCubic (h M)
fun M => special_case_lineInCubic (h M)
theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),

2
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -152,7 +152,7 @@ lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
· simp [Fin.ext_iff, δ!₂, δ!₁]
· simp [Fin.ext_iff, δ!₂, δ!₃]
· simp [Fin.ext_iff, δ!₁, δ!₃]
· exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
· exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) : ConstAbs S.val :=