Commit 2024-06-25 09:01 9389b290

View on Github →

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): add maps for division polynomials (#13399)

Estimated changes

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

added theorem WeierstrassCurve.Affine.CoordinateRing.mk_Ψ_sq

added theorem WeierstrassCurve.Affine.CoordinateRing.mk_φ

added theorem WeierstrassCurve.Affine.CoordinateRing.mk_ψ

added theorem WeierstrassCurve.Affine.CoordinateRing.mk_ψ₂_sq

added theorem WeierstrassCurve.C_Ψ₂Sq

deleted theorem WeierstrassCurve.C_Ψ₂Sq_eq

added theorem WeierstrassCurve.baseChange_preΨ'

added theorem WeierstrassCurve.baseChange_preΨ

added theorem WeierstrassCurve.baseChange_preΨ₄

added theorem WeierstrassCurve.baseChange_Φ

added theorem WeierstrassCurve.baseChange_Ψ

added theorem WeierstrassCurve.baseChange_ΨSq

added theorem WeierstrassCurve.baseChange_Ψ₂Sq

added theorem WeierstrassCurve.baseChange_Ψ₃

added theorem WeierstrassCurve.baseChange_φ

added theorem WeierstrassCurve.baseChange_ψ

added theorem WeierstrassCurve.baseChange_ψ₂

added theorem WeierstrassCurve.map_preΨ'

added theorem WeierstrassCurve.map_preΨ

added theorem WeierstrassCurve.map_preΨ₄

added theorem WeierstrassCurve.map_Φ

added theorem WeierstrassCurve.map_Ψ

added theorem WeierstrassCurve.map_ΨSq

added theorem WeierstrassCurve.map_Ψ₂Sq

added theorem WeierstrassCurve.map_Ψ₃

added theorem WeierstrassCurve.map_φ

added theorem WeierstrassCurve.map_ψ

added theorem WeierstrassCurve.map_ψ₂

added theorem WeierstrassCurve.ψ₂_sq

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

added theorem map_normEDS

added theorem map_preNormEDS'

added theorem map_preNormEDS