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

Update LineInCubic.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-20 00:19:21 +02:00
parent 1e0a0487a0
commit 1da2fd1738
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -67,7 +67,7 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
(lineInCubic_expand h g f hS 1 2) / 6
/-- We say a `LinSol` satifies `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
∀ (M : (FamilyPermutations (2 * n.succ)).group ),
lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)