Mathlib Changelog
v4
Changelog
About
Github
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