Commit 2024-05-14 00:37 9c490430

View on Github →

chore(EllipticCurve/Affine): add capitalization to Props equation and nonsingular (#12874)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

modified theorem EllipticCurve.Affine.nonsingular

added def WeierstrassCurve.Affine.Equation

added def WeierstrassCurve.Affine.Nonsingular

modified theorem WeierstrassCurve.Affine.Point.map_some

modified theorem WeierstrassCurve.Affine.Point.neg_some

modified theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yeq

modified theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne'

modified theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne

modified theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne'

modified theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne

modified theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yeq

modified theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne'

modified theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne

modified theorem WeierstrassCurve.Affine.Yeq_of_Xeq

modified theorem WeierstrassCurve.Affine.Yeq_of_Yne

modified theorem WeierstrassCurve.Affine.addPolynomial_slope

modified theorem WeierstrassCurve.Affine.derivative_addPolynomial_slope

deleted def WeierstrassCurve.Affine.equation

modified theorem WeierstrassCurve.Affine.equation_add'

modified theorem WeierstrassCurve.Affine.equation_add

modified theorem WeierstrassCurve.Affine.equation_iff'

modified theorem WeierstrassCurve.Affine.equation_neg

modified theorem WeierstrassCurve.Affine.equation_neg_iff

modified theorem WeierstrassCurve.Affine.equation_neg_of

modified theorem WeierstrassCurve.Affine.equation_zero

deleted def WeierstrassCurve.Affine.nonsingular

modified theorem WeierstrassCurve.Affine.nonsingular_add'

modified theorem WeierstrassCurve.Affine.nonsingular_add

modified theorem WeierstrassCurve.Affine.nonsingular_iff'

modified theorem WeierstrassCurve.Affine.nonsingular_iff

modified theorem WeierstrassCurve.Affine.nonsingular_neg

modified theorem WeierstrassCurve.Affine.nonsingular_neg_iff

modified theorem WeierstrassCurve.Affine.nonsingular_neg_of

modified theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero

modified theorem WeierstrassCurve.Affine.nonsingular_zero

modified theorem WeierstrassCurve.Affine.nonsingular_zero_of_Δ_ne_zero

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

modified def EllipticCurve.Affine.Point.mk

modified theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul

modified theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'

modified theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq

modified theorem WeierstrassCurve.Affine.Point.toClass_some

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

modified theorem WeierstrassCurve.Jacobian.equation_some

modified theorem WeierstrassCurve.Jacobian.nonsingular_some

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

modified theorem WeierstrassCurve.Projective.equation_some

modified theorem WeierstrassCurve.Projective.nonsingular_some