Commit 2024-08-30 15:20 c35a036e

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Projective): add API for equations and nonsingularity (#14210) This is the projective version of #13060 and is completely analogous to the current Jacobian file.

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

added theorem WeierstrassCurve.Projective.X_eq_iff

added theorem WeierstrassCurve.Projective.X_eq_of_equiv

added theorem WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Y_eq_iff

added theorem WeierstrassCurve.Projective.Y_eq_of_equiv

added theorem WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Z_eq_zero_of_equiv

added theorem WeierstrassCurve.Projective.comp_fin3

modified theorem WeierstrassCurve.Projective.equation_iff

added theorem WeierstrassCurve.Projective.equation_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.equation_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.equation_of_equiv

added theorem WeierstrassCurve.Projective.equation_smul

deleted theorem WeierstrassCurve.Projective.equation_smul_iff

modified theorem WeierstrassCurve.Projective.equation_some

modified theorem WeierstrassCurve.Projective.equation_zero

added theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq'

added theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq

added theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq

modified theorem WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero

modified theorem WeierstrassCurve.Projective.eval_polynomial

modified theorem WeierstrassCurve.Projective.eval_polynomialX

added theorem WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.eval_polynomialZ

added theorem WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.fin3_def

added theorem WeierstrassCurve.Projective.fin3_def_ext

added theorem WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero

modified theorem WeierstrassCurve.Projective.nonsingularLift_iff

deleted theorem WeierstrassCurve.Projective.nonsingularLift_zero'

modified theorem WeierstrassCurve.Projective.nonsingularLift_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.nonsingular_iff

deleted theorem WeierstrassCurve.Projective.nonsingular_iff_affine_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_of_affine_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.nonsingular_of_equiv

added theorem WeierstrassCurve.Projective.nonsingular_smul

deleted theorem WeierstrassCurve.Projective.nonsingular_smul_iff

modified theorem WeierstrassCurve.Projective.nonsingular_some

deleted theorem WeierstrassCurve.Projective.nonsingular_zero'

modified theorem WeierstrassCurve.Projective.nonsingular_zero

added theorem WeierstrassCurve.Projective.not_equiv_of_X_ne

added theorem WeierstrassCurve.Projective.not_equiv_of_Y_ne

added theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right

modified theorem WeierstrassCurve.Projective.polynomialX_eq

modified theorem WeierstrassCurve.Projective.polynomialY_eq

modified theorem WeierstrassCurve.Projective.polynomialZ_eq

modified theorem WeierstrassCurve.Projective.polynomial_relation

added theorem WeierstrassCurve.Projective.smul_eq

added theorem WeierstrassCurve.Projective.smul_equiv

modified theorem WeierstrassCurve.Projective.smul_fin3

modified theorem WeierstrassCurve.Projective.smul_fin3_ext