Commit 2026-08-14 05:10 ac1b4db2

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): add some lemmas and grind some proofs (#42477) Also rename odd to neg because odd will be reserved for odd elliptic relations.

Estimated changes

Modified Mathlib/Data/Nat/DvdSequence.lean

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

added theorem IsEllipticNet.atomRel_abs

modified theorem IsEllipticNet.atomRel_abs₁

modified theorem IsEllipticNet.atomRel_abs₂

modified theorem IsEllipticNet.atomRel_abs₃

modified theorem IsEllipticNet.atomRel_avg_sub

modified theorem IsEllipticNet.atomRel_eq

added theorem IsEllipticNet.atomRel_even

added theorem IsEllipticNet.atomRel_neg

modified theorem IsEllipticNet.atomRel_neg₁

modified theorem IsEllipticNet.atomRel_neg₂

modified theorem IsEllipticNet.atomRel_neg₃

added theorem IsEllipticNet.atomRel_odd

modified theorem IsEllipticNet.atomRel_same₁₃

modified theorem IsEllipticNet.atomRel_same₁₄

modified theorem IsEllipticNet.atomRel_same₂₄

modified theorem IsEllipticNet.atom_abs_left

modified theorem IsEllipticNet.atom_mul_atom

modified theorem IsEllipticNet.atom_neg_left

modified theorem IsEllipticNet.neg_atom

added theorem IsEllipticNet.neg_atomRel₁₂

added theorem IsEllipticNet.neg_atomRel₂₃

added theorem IsEllipticNet.neg_atomRel₃₄

modified theorem IsEllipticNet.rel_neg

added theorem normEDS_atomRel_even

added theorem normEDS_atomRel_odd