Commit 2025-05-19 14:18 406d494b

View on Github →

chore(NumberTheory/EllipticDivisibilitySequence): simplify proofs and deprecate lemmas (#24964) Simplify proofs with terminal rws to terminal simps and deprecate even/odd_ofNat lemmas.

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

deleted theorem WeierstrassCurve.preΨ_even_ofNat

deleted theorem WeierstrassCurve.preΨ_odd_ofNat

deleted theorem WeierstrassCurve.ΨSq_even_ofNat

deleted theorem WeierstrassCurve.ΨSq_odd_ofNat

deleted theorem WeierstrassCurve.Ψ_even_ofNat

deleted theorem WeierstrassCurve.Ψ_odd_ofNat

deleted theorem WeierstrassCurve.ψ_even_ofNat

deleted theorem WeierstrassCurve.ψ_odd_ofNat

Modified Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

deleted theorem normEDS_even_ofNat

deleted theorem normEDS_odd_ofNat

modified def preNormEDS'

deleted theorem preNormEDS_even_ofNat

deleted theorem preNormEDS_odd_ofNat