Commit 2024-06-09 22:24 c74732f1

View on Github →

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): define division polynomials (#6703)

Estimated changes

Modified Mathlib.lean

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

added theorem WeierstrassCurve.C_Ψ₂Sq_eq

added theorem WeierstrassCurve.preΨ'_even

added theorem WeierstrassCurve.preΨ'_four

added theorem WeierstrassCurve.preΨ'_odd

added theorem WeierstrassCurve.preΨ'_one

added theorem WeierstrassCurve.preΨ'_three

added theorem WeierstrassCurve.preΨ'_two

added theorem WeierstrassCurve.preΨ'_zero

added theorem WeierstrassCurve.preΨ_even

added theorem WeierstrassCurve.preΨ_four

added theorem WeierstrassCurve.preΨ_neg

added theorem WeierstrassCurve.preΨ_odd

added theorem WeierstrassCurve.preΨ_ofNat

added theorem WeierstrassCurve.preΨ_one

added theorem WeierstrassCurve.preΨ_three

added theorem WeierstrassCurve.preΨ_two

added theorem WeierstrassCurve.preΨ_zero

added theorem WeierstrassCurve.Φ_four

added theorem WeierstrassCurve.Φ_neg

added theorem WeierstrassCurve.Φ_ofNat

added theorem WeierstrassCurve.Φ_one

added theorem WeierstrassCurve.Φ_three

added theorem WeierstrassCurve.Φ_two

added theorem WeierstrassCurve.Φ_zero

added theorem WeierstrassCurve.ΨSq_even

added theorem WeierstrassCurve.ΨSq_four

added theorem WeierstrassCurve.ΨSq_neg

added theorem WeierstrassCurve.ΨSq_odd

added theorem WeierstrassCurve.ΨSq_ofNat

added theorem WeierstrassCurve.ΨSq_one

added theorem WeierstrassCurve.ΨSq_three

added theorem WeierstrassCurve.ΨSq_two

added theorem WeierstrassCurve.ΨSq_zero

added theorem WeierstrassCurve.Ψ_even

added theorem WeierstrassCurve.Ψ_four

added theorem WeierstrassCurve.Ψ_neg

added theorem WeierstrassCurve.Ψ_odd

added theorem WeierstrassCurve.Ψ_ofNat

added theorem WeierstrassCurve.Ψ_one

added theorem WeierstrassCurve.Ψ_three

added theorem WeierstrassCurve.Ψ_two

added theorem WeierstrassCurve.Ψ_zero

added theorem WeierstrassCurve.Ψ₂Sq_eq

added theorem WeierstrassCurve.φ_four

added theorem WeierstrassCurve.φ_neg

added theorem WeierstrassCurve.φ_one

added theorem WeierstrassCurve.φ_three

added theorem WeierstrassCurve.φ_two

added theorem WeierstrassCurve.φ_zero

added theorem WeierstrassCurve.ψ_even

added theorem WeierstrassCurve.ψ_four

added theorem WeierstrassCurve.ψ_neg

added theorem WeierstrassCurve.ψ_odd

added theorem WeierstrassCurve.ψ_one

added theorem WeierstrassCurve.ψ_three

added theorem WeierstrassCurve.ψ_two

added theorem WeierstrassCurve.ψ_zero

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

modified theorem normEDS_neg