Commit 2024-05-28 09:02 5ddf48f5

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Jacobian): add API for equations and nonsingularity (#13060)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

added theorem WeierstrassCurve.Jacobian.X_eq_of_equiv

added theorem WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Y_eq_of_equiv

added theorem WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv

modified theorem WeierstrassCurve.Jacobian.equation_iff

added theorem WeierstrassCurve.Jacobian.equation_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.equation_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.equation_of_equiv

modified theorem WeierstrassCurve.Jacobian.equation_smul_iff

modified theorem WeierstrassCurve.Jacobian.equation_some

deleted theorem WeierstrassCurve.Jacobian.equation_zero'

modified theorem WeierstrassCurve.Jacobian.equation_zero

added theorem WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq

modified theorem WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero

modified theorem WeierstrassCurve.Jacobian.eval_polynomial

modified theorem WeierstrassCurve.Jacobian.eval_polynomialX

added theorem WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.eval_polynomialZ

added theorem WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.fin3_def

added theorem WeierstrassCurve.Jacobian.fin3_def_ext

modified theorem WeierstrassCurve.Jacobian.nonsingularLift_iff

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_zero'

modified theorem WeierstrassCurve.Jacobian.nonsingularLift_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_affine_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.nonsingular_iff

deleted theorem WeierstrassCurve.Jacobian.nonsingular_iff_affine_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_of_affine_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.nonsingular_of_equiv

added theorem WeierstrassCurve.Jacobian.nonsingular_smul

deleted theorem WeierstrassCurve.Jacobian.nonsingular_smul_iff

modified theorem WeierstrassCurve.Jacobian.nonsingular_some

deleted theorem WeierstrassCurve.Jacobian.nonsingular_zero'

modified theorem WeierstrassCurve.Jacobian.nonsingular_zero

added theorem WeierstrassCurve.Jacobian.not_equiv_of_X_ne

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Y_ne

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right

modified theorem WeierstrassCurve.Jacobian.polynomialX_eq

modified theorem WeierstrassCurve.Jacobian.polynomialY_eq

modified theorem WeierstrassCurve.Jacobian.polynomialZ_eq

added theorem WeierstrassCurve.Jacobian.smul_eq

added theorem WeierstrassCurve.Jacobian.smul_equiv

modified theorem WeierstrassCurve.Jacobian.smul_fin3