Basic

📁 Source: Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Basic.lean

Statistics

Metric	Count
Definitions Equation, Nonsingular, polynomial, polynomialX, polynomialY, toAffine	6
Theorems baseChange, map, baseChange_equation, baseChange_nonsingular, baseChange_polynomial, baseChange_polynomialX, baseChange_polynomialY, degree_polynomial, equation_iff, equation_iff', equation_iff_nonsingular, equation_iff_nonsingular_of_Δ_ne_zero, equation_iff_variableChange, equation_zero, evalEval_polynomial, evalEval_polynomialX, evalEval_polynomialX_zero, evalEval_polynomialY, evalEval_polynomialY_zero, evalEval_polynomial_zero, irreducible_polynomial, map_equation, map_nonsingular, map_polynomial, map_polynomialX, map_polynomialY, monic_polynomial, natDegree_polynomial, nonsingular_iff, nonsingular_iff', nonsingular_iff_variableChange, nonsingular_zero, polynomial_eq, polynomial_ne_zero	34
Total	40

WeierstrassCurve

Definitions

Name	Category	Theorems
toAffine 📖	CompOp	36 math math: Affine.baseChange_nonsingular, ψ₂_sq, Affine.map_polynomialY, Affine.map_addY, Affine.baseChange_negY, Affine.baseChange_negPolynomial, Affine.map_negPolynomial, Affine.nonsingular_iff_variableChange, Affine.equation_iff_variableChange, C_Ψ₂Sq, Affine.map_slope, Affine.CoordinateRing.map_mk, Affine.baseChange_addPolynomial, Affine.map_polynomial, Affine.baseChange_polynomialX, Affine.map_nonsingular, Affine.baseChange_equation, Affine.CoordinateRing.map_injective, Affine.baseChange_polynomial, Affine.map_negAddY, Affine.map_equation, Affine.Point.map_some, Affine.map_polynomialX, Affine.baseChange_slope, Affine.baseChange_addY, Affine.Equation.map, Affine.Equation.baseChange, Affine.map_addPolynomial, Affine.map_negY, Affine.baseChange_polynomialY, Affine.baseChange_addX, Affine.CoordinateRing.map_smul, Affine.equation_iff_nonsingular, Affine.map_addX, Affine.baseChange_negAddY, Ψ_odd

WeierstrassCurve.Affine

Definitions

Name	Category	Theorems
Equation 📖	MathDef	28 math math: pointEquiv_symm_some, pointEquiv_some, equation_iff', equation_iff_variableChange, equation_iff_nonsingular_of_Δ_ne_zero, equation_zero, equation_neg, equation_add_iff, pointEquivSubtype_some, baseChange_equation, map_equation, equation_iff, pointEquivSubtype_symm_some, pointEquiv_zero, equation_negAdd, Equation.map, WeierstrassCurve.Jacobian.equation_some, Equation.baseChange, nonsingular_iff', WeierstrassCurve.Jacobian.equation_of_Z_ne_zero, equation_iff_nonsingular, pointEquivSubtype_symm_none, pointEquivSubtype_zero, WeierstrassCurve.Projective.equation_some, pointEquiv_symm_none, nonsingular_iff, WeierstrassCurve.Projective.equation_of_Z_ne_zero, equation_add
Nonsingular 📖	MathDef	39 math math: nonsingular_negAdd, baseChange_nonsingular, WeierstrassCurve.Jacobian.Point.toAffineLift_some, WeierstrassCurve.Projective.nonsingularLift_some, WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero, nonsingularPointEquivSubtype_symm_none, WeierstrassCurve.Projective.Point.toAffine_some, WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero, WeierstrassCurve.Jacobian.Point.fromAffine_some, nonsingular_zero, CoordinateRing.mk_XYIdeal'_neg_mul, WeierstrassCurve.Projective.Point.toAffineLift_some, nonsingular_iff_variableChange, WeierstrassCurve.Jacobian.nonsingularLift_some, equation_iff_nonsingular_of_Δ_ne_zero, WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_ne_zero, Point.neg_some, WeierstrassCurve.Projective.Point.fromAffine_some, WeierstrassCurve.Jacobian.Point.toAffine_some, nonsingular_add, map_nonsingular, nonsingularPointEquivSubtype_symm_some, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, nonsingularPointEquiv_some, nonsingularPointEquiv_symm_some, WeierstrassCurve.Jacobian.nonsingular_some, Point.map_some, WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingular_some, nonsingularPointEquivSubtype_some, nonsingular_iff', equation_iff_nonsingular, nonsingularPointEquiv_zero, nonsingularPointEquivSubtype_zero, nonsingular_iff, nonsingularPointEquiv_symm_none, nonsingular_neg, nonsingular_negAdd_of_eval_derivative_ne_zero
polynomial 📖	CompOp	48 math math: CoordinateRing.smul, monic_polynomial, CoordinateRing.basis_one, WeierstrassCurve.ψ₂_sq, CoordinateRing.smul_basis_mul_C, CoordinateRing.coe_basis, Point.toClass_zero, C_addPolynomial, irreducible_polynomial, polynomial_eq, natDegree_polynomial, CoordinateRing.instIsScalarTowerPolynomial, CoordinateRing.mk_ψ, CoordinateRing.C_addPolynomial, CoordinateRing.mk_XYIdeal'_neg_mul, CoordinateRing.XYIdeal_add_eq, CoordinateRing.norm_smul_basis, CoordinateRing.degree_norm_smul_basis, WeierstrassCurve.C_Ψ₂Sq, CoordinateRing.map_mk, CoordinateRing.mk_φ, evalEval_polynomial_zero, CoordinateRing.instIsDomain, CoordinateRing.mk_Ψ_sq, map_polynomial, CoordinateRing.XYIdeal_neg_mul, CoordinateRing.exists_smul_basis_eq, CoordinateRing.C_addPolynomial_slope, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', degree_polynomial, CoordinateRing.map_injective, baseChange_polynomial, Point.toClass_some, Point.toClass_injective, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, CoordinateRing.coe_norm_smul_basis, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, CoordinateRing.mk_ψ₂_sq, CoordinateRing.basis_zero, evalEval_polynomial, Point.toClass_eq_zero, CoordinateRing.XYIdeal'_eq, CoordinateRing.map_smul, WeierstrassCurve.Ψ_odd, CoordinateRing.basis_apply, Point.toClass_apply, CoordinateRing.smul_basis_mul_Y, CoordinateRing.XYIdeal_mul_XYIdeal
polynomialX 📖	CompOp	7 math math: WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, baseChange_polynomialX, slope_of_Y_ne_eq_evalEval, map_polynomialX, evalEval_polynomialX, evalEval_polynomialX_zero
polynomialY 📖	CompOp	9 math math: Y_sub_negPolynomial, map_polynomialY, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, Y_sub_polynomialY, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, evalEval_polynomialY_zero, slope_of_Y_ne_eq_evalEval, evalEval_polynomialY, baseChange_polynomialY

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_equation 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Equation WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	map_equation AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.toRingHom_eq_coe WeierstrassCurve.map_baseChange RingHom.coe_coe
baseChange_nonsingular 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Nonsingular WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	map_nonsingular AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.toRingHom_eq_coe WeierstrassCurve.map_baseChange RingHom.coe_coe
baseChange_polynomial 📖	mathematical	—	polynomial WeierstrassCurve.toAffine WeierstrassCurve.baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomial WeierstrassCurve.map_baseChange
baseChange_polynomialX 📖	mathematical	—	polynomialX WeierstrassCurve.toAffine WeierstrassCurve.baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomialX WeierstrassCurve.map_baseChange
baseChange_polynomialY 📖	mathematical	—	polynomialY WeierstrassCurve.toAffine WeierstrassCurve.baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomialY WeierstrassCurve.map_baseChange
degree_polynomial 📖	mathematical	—	Polynomial.degree Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring polynomial WithBot instOfNatAtLeastTwo WithBot.natCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat polynomial_eq Cubic.degree_of_b_ne_zero' one_ne_zero NeZero.one Polynomial.nontrivial
equation_iff 📖	mathematical	—	Equation Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	equation_iff' sub_eq_zero
equation_iff' 📖	mathematical	—	Equation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Equation.eq_1 evalEval_polynomial
equation_iff_nonsingular 📖	mathematical	—	Equation WeierstrassCurve.toAffine Nonsingular	—	equation_iff_nonsingular_of_Δ_ne_zero Units.ne_zero WeierstrassCurve.coe_Δ'
equation_iff_nonsingular_of_Δ_ne_zero 📖	mathematical	—	Equation Nonsingular	—	equation_iff_variableChange nonsingular_iff_variableChange WeierstrassCurve.variableChange_Δ inv_one Units.val_one one_pow one_mul
equation_iff_variableChange 📖	mathematical	—	Equation WeierstrassCurve.toAffine WeierstrassCurve.VariableChange WeierstrassCurve.Affine WeierstrassCurve.instSMulVariableChange Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	equation_iff' neg_eq_zero equation_zero WeierstrassCurve.variableChange_a₆ inv_one Units.val_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Nat.cast_one
equation_zero 📖	mathematical	—	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₆	—	Equation.eq_1 evalEval_polynomial_zero neg_eq_zero
evalEval_polynomial 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring polynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Polynomial.eval_sub Polynomial.eval_add Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_mul Polynomial.eval_C add_mul Distrib.rightDistribClass add_assoc
evalEval_polynomialX 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring polynomialX SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₁ Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WeierstrassCurve.a₂ WeierstrassCurve.a₄	—	Nat.instAtLeastTwoHAddOfNat Polynomial.eval_sub Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X Polynomial.eval_add Polynomial.eval_pow
evalEval_polynomialX_zero 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing polynomialX NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing WeierstrassCurve.a₄	—	Nat.instAtLeastTwoHAddOfNat evalEval_polynomialX MulZeroClass.mul_zero zero_pow zero_add zero_sub
evalEval_polynomialY 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring polynomialY Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₁ WeierstrassCurve.a₃	—	Nat.instAtLeastTwoHAddOfNat Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X add_assoc
evalEval_polynomialY_zero 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing polynomialY WeierstrassCurve.a₃	—	Nat.instAtLeastTwoHAddOfNat evalEval_polynomialY MulZeroClass.mul_zero zero_add
evalEval_polynomial_zero 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing polynomial NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing WeierstrassCurve.a₆	—	evalEval_polynomial zero_pow MulZeroClass.mul_zero zero_add zero_sub
irreducible_polynomial 📖	mathematical	—	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero polynomial	—	Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors monic_polynomial natDegree_polynomial IsDomain.toNontrivial LE.le.not_gt LE.le.trans Eq.le polynomial_eq Cubic.coeff_eq_c Cubic.degree_of_b_eq_zero' Nat.instAtLeastTwoHAddOfNat Nat.WithBot.add_eq_three_iff Polynomial.degree_mul Cubic.degree_of_a_ne_zero' neg_ne_zero one_ne_zero' NeZero.one Cubic.coeff_eq_d Polynomial.degree_add_eq_right_of_degree_lt Polynomial.degree_add_eq_left_of_degree_lt
map_equation 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	Equation WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_polynomial Polynomial.map_mapRingHom_evalEval map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_nonsingular 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	Nonsingular WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_equation map_polynomialX Polynomial.map_mapRingHom_evalEval map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_polynomialY
map_polynomial 📖	mathematical	—	polynomial WeierstrassCurve.toAffine WeierstrassCurve.map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.map_sub Polynomial.map_add Polynomial.map_pow Polynomial.map_X Polynomial.map_mul Polynomial.map_C
map_polynomialX 📖	mathematical	—	polynomialX WeierstrassCurve.toAffine WeierstrassCurve.map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	map_ofNat RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.map_sub Polynomial.map_mul Polynomial.map_C Polynomial.map_X Polynomial.map_add Polynomial.map_ofNat Polynomial.map_pow
map_polynomialY 📖	mathematical	—	polynomialY WeierstrassCurve.toAffine WeierstrassCurve.map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	map_ofNat RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Polynomial.map_add Polynomial.map_mul Polynomial.map_ofNat Polynomial.map_X Polynomial.map_C
monic_polynomial 📖	mathematical	—	Polynomial.Monic Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring polynomial	—	polynomial_eq Cubic.monic_of_b_eq_one'
natDegree_polynomial 📖	mathematical	—	Polynomial.natDegree Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring polynomial	—	polynomial_eq Cubic.natDegree_of_b_ne_zero' one_ne_zero NeZero.one Polynomial.nontrivial
nonsingular_iff 📖	mathematical	—	Nonsingular Equation	—	Nat.instAtLeastTwoHAddOfNat nonsingular_iff' sub_ne_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add
nonsingular_iff' 📖	mathematical	—	Nonsingular Equation	—	Nat.instAtLeastTwoHAddOfNat Nonsingular.eq_1 equation_iff' evalEval_polynomialX evalEval_polynomialY
nonsingular_iff_variableChange 📖	mathematical	—	Nonsingular WeierstrassCurve.toAffine WeierstrassCurve.VariableChange WeierstrassCurve.Affine WeierstrassCurve.instSMulVariableChange Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Nat.instAtLeastTwoHAddOfNat nonsingular_iff' equation_iff_variableChange equation_zero neg_ne_zero nonsingular_zero WeierstrassCurve.variableChange_a₃ WeierstrassCurve.variableChange_a₄ inv_one Units.val_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Nat.cast_one Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
nonsingular_zero 📖	mathematical	—	Nonsingular MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₆	—	Nonsingular.eq_1 equation_zero evalEval_polynomialX_zero neg_ne_zero evalEval_polynomialY_zero
polynomial_eq 📖	mathematical	—	polynomial Cubic.toPoly Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instZero Polynomial.instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₁ WeierstrassCurve.a₃ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg Polynomial.C_0 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one
polynomial_ne_zero 📖	—	—	—	—	polynomial_eq Cubic.ne_zero_of_b_ne_zero one_ne_zero NeZero.one Polynomial.nontrivial

WeierstrassCurve.Affine.Equation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	WeierstrassCurve.Affine.Equation WeierstrassCurve.toAffine WeierstrassCurve.baseChange	WeierstrassCurve.Affine.Equation WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.toRingHom_eq_coe WeierstrassCurve.map_baseChange map
map 📖	mathematical	WeierstrassCurve.Affine.Equation	WeierstrassCurve.Affine.Equation WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	eq_1 WeierstrassCurve.Affine.map_polynomial Polynomial.map_mapRingHom_evalEval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index