Commit 2026-07-07 10:41 2e09891a

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): add elliptic nets (#25989) This PR continues the work from #25030. Original PR: https://github.com/leanprover-community/mathlib4/pull/25030

Estimated changes

deleted theorem IsEllDivSequence.smul
deleted def IsEllDivSequence
deleted theorem IsEllSequence.smul
deleted def IsEllSequence
added theorem IsEllipticNet.atom_odd
added theorem IsEllipticNet.map_atom
added theorem IsEllipticNet.map_rel
added theorem IsEllipticNet.neg_atom
added theorem IsEllipticNet.rel_eq
added theorem IsEllipticNet.rel_even
added theorem IsEllipticNet.rel_neg
added theorem IsEllipticNet.rel_odd
added def IsEllipticNet
deleted theorem isEllDivSequence_id
deleted theorem isEllSequence_id