Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-02 17:04 c06c6806

View on Github →

feat(algebraic_geometry/EllipticCurve): add 2-torsion polynomials and changes of variables (#15230)

Estimated changes

Modified src/algebraic_geometry/EllipticCurve.lean

deleted def EllipticCurve.b2

deleted def EllipticCurve.b4

deleted def EllipticCurve.b6

deleted def EllipticCurve.b8

added theorem EllipticCurve.b_relation

added def EllipticCurve.b₂

added def EllipticCurve.b₄

added def EllipticCurve.b₆

added def EllipticCurve.b₈

deleted def EllipticCurve.c4

deleted theorem EllipticCurve.c4_def

added theorem EllipticCurve.c_relation

added theorem EllipticCurve.change_of_variable.a₁_eq

added theorem EllipticCurve.change_of_variable.a₂_eq

added theorem EllipticCurve.change_of_variable.a₃_eq

added theorem EllipticCurve.change_of_variable.a₄_eq

added theorem EllipticCurve.change_of_variable.a₆_eq

added theorem EllipticCurve.change_of_variable.b₂_eq

added theorem EllipticCurve.change_of_variable.b₄_eq

added theorem EllipticCurve.change_of_variable.b₆_eq

added theorem EllipticCurve.change_of_variable.b₈_eq

added theorem EllipticCurve.change_of_variable.c₄_eq

added theorem EllipticCurve.change_of_variable.c₆_eq

added theorem EllipticCurve.change_of_variable.j_eq

added theorem EllipticCurve.change_of_variable.Δ_eq

added def EllipticCurve.change_of_variable

added theorem EllipticCurve.coe_Δ

added def EllipticCurve.c₄

added def EllipticCurve.c₆

deleted def EllipticCurve.disc

deleted def EllipticCurve.disc_aux

deleted theorem EllipticCurve.disc_aux_def

deleted theorem EllipticCurve.disc_def

deleted theorem EllipticCurve.disc_is_unit

modified def EllipticCurve.j

added theorem EllipticCurve.two_torsion_polynomial.disc_eq

added theorem EllipticCurve.two_torsion_polynomial.disc_ne_zero

added def EllipticCurve.two_torsion_polynomial

added def EllipticCurve.Δ_aux

modified structure EllipticCurve