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:52 +01:00
parent 748188f81a
commit 6589b45edf
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/Odd/LineInCubic.lean
View file

@ -123,7 +123,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
rw [P_P_P!_accCube' g f hfg] at h1
simp only [Nat.succ_eq_add_one, 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 ?_)