Commit 2024-06-17 16:07 459cd285

View on Github →

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): compute degrees of division polynomials (#10878)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Int.lean

added theorem Int.not_even_two_mul_add_one

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

added theorem WeierstrassCurve.coeff_preΨ'

added theorem WeierstrassCurve.coeff_preΨ

added theorem WeierstrassCurve.coeff_preΨ₄

added theorem WeierstrassCurve.coeff_Φ

added theorem WeierstrassCurve.coeff_ΨSq

added theorem WeierstrassCurve.coeff_Ψ₂Sq

added theorem WeierstrassCurve.coeff_Ψ₃

added theorem WeierstrassCurve.natDegree_preΨ'

added theorem WeierstrassCurve.natDegree_preΨ

added theorem WeierstrassCurve.natDegree_preΨ₄

added theorem WeierstrassCurve.natDegree_Φ

added theorem WeierstrassCurve.natDegree_ΨSq

added theorem WeierstrassCurve.natDegree_Ψ₂Sq

added theorem WeierstrassCurve.natDegree_Ψ₃