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 2025-01-23 01:15:49 +01:00
parent 0cc03c09ad
commit 748188f81a
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

@ -136,7 +136,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
rw [P_P_P!_accCube' g f hfg] at h1
simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1
cases h1 <;> rename_i h1
· apply Or.inl
· left
linear_combination h1
· cases h1 <;> rename_i h1
· refine Or.inr (Or.inl ?_)