Commit 2023-06-28 01:50 1ecea4a9

View on Github →

feat: port AlgebraicGeometry.EllipticCurve.Weierstrass (#5294)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

added def EllipticCurve.baseChange

added theorem EllipticCurve.baseChange_j

added theorem EllipticCurve.coeBaseChange_Δ'

added theorem EllipticCurve.coe_inv_baseChange_Δ'

added theorem EllipticCurve.coe_inv_variableChange_Δ'

added theorem EllipticCurve.coe_variableChange_Δ'

added def EllipticCurve.j

added theorem EllipticCurve.nonsingular

added theorem EllipticCurve.twoTorsionPolynomial_disc_ne_zero

added def EllipticCurve.variableChange

added theorem EllipticCurve.variableChange_j

added structure EllipticCurve

added theorem WeierstrassCurve.CoordinateRing.XClass_ne_zero

added theorem WeierstrassCurve.CoordinateRing.YClass_ne_zero

added theorem WeierstrassCurve.CoordinateRing.basis_apply

added theorem WeierstrassCurve.CoordinateRing.basis_one

added theorem WeierstrassCurve.CoordinateRing.basis_zero

added theorem WeierstrassCurve.CoordinateRing.coe_basis

added theorem WeierstrassCurve.CoordinateRing.coe_norm_smul_basis

added theorem WeierstrassCurve.CoordinateRing.degree_norm_ne_one

added theorem WeierstrassCurve.CoordinateRing.degree_norm_smul_basis

added theorem WeierstrassCurve.CoordinateRing.exists_smul_basis_eq

added theorem WeierstrassCurve.CoordinateRing.natDegree_norm_ne_one

added theorem WeierstrassCurve.CoordinateRing.norm_smul_basis

added theorem WeierstrassCurve.CoordinateRing.smul

added theorem WeierstrassCurve.CoordinateRing.smul_basis_eq_zero

added theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_C

added theorem WeierstrassCurve.CoordinateRing.smul_basis_mul_Y

added theorem WeierstrassCurve.b_relation

added def WeierstrassCurve.baseChange

added theorem WeierstrassCurve.baseChange_baseChange

added theorem WeierstrassCurve.baseChange_b₂

added theorem WeierstrassCurve.baseChange_b₄

added theorem WeierstrassCurve.baseChange_b₆

added theorem WeierstrassCurve.baseChange_b₈

added theorem WeierstrassCurve.baseChange_c₄

added theorem WeierstrassCurve.baseChange_c₆

added theorem WeierstrassCurve.baseChange_self

added theorem WeierstrassCurve.baseChange_Δ

added def WeierstrassCurve.b₂

added def WeierstrassCurve.b₄

added def WeierstrassCurve.b₆

added def WeierstrassCurve.b₈

added theorem WeierstrassCurve.c_relation

added def WeierstrassCurve.c₄

added def WeierstrassCurve.c₆

added theorem WeierstrassCurve.degree_polynomial

added theorem WeierstrassCurve.equation_iff'

added theorem WeierstrassCurve.equation_iff

added theorem WeierstrassCurve.equation_iff_baseChange

added theorem WeierstrassCurve.equation_iff_baseChange_of_baseChange

added theorem WeierstrassCurve.equation_iff_variableChange

added theorem WeierstrassCurve.equation_zero

added theorem WeierstrassCurve.eval_polynomial

added theorem WeierstrassCurve.eval_polynomialX

added theorem WeierstrassCurve.eval_polynomialX_zero

added theorem WeierstrassCurve.eval_polynomialY

added theorem WeierstrassCurve.eval_polynomialY_zero

added theorem WeierstrassCurve.eval_polynomial_zero

added theorem WeierstrassCurve.irreducible_polynomial

added theorem WeierstrassCurve.monic_polynomial

added theorem WeierstrassCurve.natDegree_polynomial

added theorem WeierstrassCurve.nonsingular_iff'

added theorem WeierstrassCurve.nonsingular_iff

added theorem WeierstrassCurve.nonsingular_iff_baseChange

added theorem WeierstrassCurve.nonsingular_iff_baseChange_of_baseChange

added theorem WeierstrassCurve.nonsingular_iff_variableChange

added theorem WeierstrassCurve.nonsingular_of_Δ_ne_zero

added theorem WeierstrassCurve.nonsingular_zero

added theorem WeierstrassCurve.nonsingular_zero_of_Δ_ne_zero

added theorem WeierstrassCurve.polynomial_eq

added theorem WeierstrassCurve.polynomial_ne_zero

added def WeierstrassCurve.twoTorsionPolynomial

added theorem WeierstrassCurve.twoTorsionPolynomial_disc

added theorem WeierstrassCurve.twoTorsionPolynomial_disc_isUnit

added theorem WeierstrassCurve.twoTorsionPolynomial_disc_ne_zero

added def WeierstrassCurve.variableChange

added theorem WeierstrassCurve.variableChange_b₂

added theorem WeierstrassCurve.variableChange_b₄

added theorem WeierstrassCurve.variableChange_b₆

added theorem WeierstrassCurve.variableChange_b₈

added theorem WeierstrassCurve.variableChange_c₄

added theorem WeierstrassCurve.variableChange_c₆

added theorem WeierstrassCurve.variableChange_Δ

added def WeierstrassCurve.Δ

added structure WeierstrassCurve

Modified Mathlib/RingTheory/Polynomial/Quotient.lean