Commit 2024-11-29 11:09 90f062fe

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786) Provide a quick proof that normalised EDSs satisfy an even-odd recursion over all integers rather than just natural numbers, without relying on heavier machinery i.e. the full EDS recurrence in #13155, and make Int.negInduction slightly stronger.

Estimated changes

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

modified theorem WeierstrassCurve.preΨ_even

added theorem WeierstrassCurve.preΨ_even_ofNat

modified theorem WeierstrassCurve.preΨ_odd

added theorem WeierstrassCurve.preΨ_odd_ofNat

modified theorem WeierstrassCurve.ΨSq_even

added theorem WeierstrassCurve.ΨSq_even_ofNat

modified theorem WeierstrassCurve.ΨSq_odd

added theorem WeierstrassCurve.ΨSq_odd_ofNat

modified theorem WeierstrassCurve.Ψ_even

added theorem WeierstrassCurve.Ψ_even_ofNat

modified theorem WeierstrassCurve.Ψ_odd

added theorem WeierstrassCurve.Ψ_odd_ofNat

modified theorem WeierstrassCurve.ψ_even

added theorem WeierstrassCurve.ψ_even_ofNat

modified theorem WeierstrassCurve.ψ_odd

added theorem WeierstrassCurve.ψ_odd_ofNat

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

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/Nat/Cast/Defs.lean

added theorem Nat.cast_four

added theorem Nat.cast_three

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

modified theorem normEDS_even

added theorem normEDS_even_ofNat

modified theorem normEDS_odd

added theorem normEDS_odd_ofNat

modified theorem preNormEDS_even

added theorem preNormEDS_even_ofNat

modified theorem preNormEDS_odd

added theorem preNormEDS_odd_ofNat