Basic

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

Statistics

Metric	Count
Definitions Equation, Nonsingular, NonsingularLift, PointClass, instMulActionForallFinOfNatNat, instSMulForallFinOfNatNat, instSetoidForallFinOfNatNat, polynomial, polynomialX, polynomialY, polynomialZ, toAffine, toJacobian	13
Theorems baseChange, map, X_eq_iff, X_eq_of_equiv, X_ne_zero_of_Z_eq_zero, Y_eq_iff, Y_eq_of_equiv, Y_ne_zero_of_Z_eq_zero, Z_eq_zero_of_equiv, baseChange_equation, baseChange_nonsingular, baseChange_polynomial, baseChange_polynomialX, baseChange_polynomialY, baseChange_polynomialZ, comp_equiv_comp, comp_fin3, comp_smul, equation_iff, equation_of_Z_eq_zero, equation_of_Z_ne_zero, equation_of_equiv, equation_smul, equation_some, equation_zero, equiv_iff_eq_of_Z_eq, equiv_iff_eq_of_Z_eq', equiv_of_X_eq_of_Y_eq, equiv_of_Z_eq_zero, equiv_some_of_Z_ne_zero, equiv_zero_of_Z_eq_zero, eval_polynomial, eval_polynomialX, eval_polynomialX_of_Z_ne_zero, eval_polynomialY, eval_polynomialY_of_Z_ne_zero, eval_polynomialZ, eval_polynomial_of_Z_ne_zero, fin3_def, fin3_def_ext, isUnit_X_of_Z_eq_zero, isUnit_Y_of_Z_eq_zero, map_equation, map_nonsingular, map_polynomial, map_polynomialX, map_polynomialY, map_polynomialZ, nonsingularLift_iff, nonsingularLift_some, nonsingularLift_zero, nonsingular_iff, nonsingular_iff_of_Z_ne_zero, nonsingular_of_Z_eq_zero, nonsingular_of_Z_ne_zero, nonsingular_of_equiv, nonsingular_smul, nonsingular_some, nonsingular_zero, not_equiv_of_X_ne, not_equiv_of_Y_ne, not_equiv_of_Z_eq_zero_left, not_equiv_of_Z_eq_zero_right, polynomialX_eq, polynomialY_eq, polynomialZ_eq, polynomial_relation, smul_eq, smul_equiv, smul_equiv_smul, smul_fin3, smul_fin3_ext	72
Total	85

WeierstrassCurve

Definitions

Name	Category	Theorems
toJacobian 📖	CompOp	40 math math: Jacobian.map_addX, Jacobian.baseChange_add, Jacobian.map_equation, Jacobian.map_dblX, Jacobian.baseChange_polynomialZ, Jacobian.map_negDblY, Jacobian.map_negY, Jacobian.map_dblZ, Jacobian.baseChange_nonsingular, Jacobian.baseChange_addX, Jacobian.map_add, Jacobian.baseChange_equation, Jacobian.baseChange_addXYZ, Jacobian.baseChange_dblX, Jacobian.baseChange_negDblY, Jacobian.baseChange_polynomialY, Jacobian.baseChange_dblY, Jacobian.map_dblXYZ, Jacobian.map_addY, Jacobian.baseChange_dblU, Jacobian.baseChange_polynomial, Jacobian.map_nonsingular, Jacobian.baseChange_neg, Jacobian.baseChange_dblXYZ, Jacobian.map_polynomialZ, Jacobian.Equation.baseChange, Jacobian.baseChange_dblZ, Jacobian.baseChange_polynomialX, Jacobian.Equation.map, Jacobian.map_negAddY, Jacobian.map_polynomial, Jacobian.map_dblY, Jacobian.map_dblU, Jacobian.baseChange_negY, Jacobian.map_polynomialY, Jacobian.baseChange_addY, Jacobian.map_polynomialX, Jacobian.map_neg, Jacobian.map_addXYZ, Jacobian.baseChange_negAddY

WeierstrassCurve.Jacobian

Definitions

Name	Category	Theorems
Equation 📖	MathDef	15 math math: nonsingular_iff_of_Y_eq_negY, map_equation, equation_of_equiv, baseChange_equation, nonsingular_of_Z_eq_zero, equation_iff, Equation.baseChange, equation_of_Z_eq_zero, Equation.map, equation_smul, equation_zero, equation_some, equation_of_Z_ne_zero, nonsingular_iff, nonsingular_iff_of_Z_ne_zero
Nonsingular 📖	MathDef	18 math math: nonsingular_iff_of_Y_eq_negY, Point.toAffineLift_some, Point.toAffine_of_Z_ne_zero, nonsingularLift_iff, baseChange_nonsingular, nonsingular_add, Point.toAffineLift_of_Z_ne_zero, nonsingular_of_Z_eq_zero, map_nonsingular, nonsingular_smul, Point.toAffine_some, nonsingular_neg, nonsingular_some, nonsingular_of_Z_ne_zero, nonsingular_zero, nonsingular_of_equiv, nonsingular_iff, nonsingular_iff_of_Z_ne_zero
NonsingularLift 📖	MathDef	7 math math: nonsingularLift_addMap, Point.nonsingular, Point.fromAffine_some, nonsingularLift_iff, nonsingularLift_some, nonsingularLift_zero, nonsingularLift_negMap
PointClass 📖	CompOp	—
instMulActionForallFinOfNatNat 📖	CompOp	19 math math: Point.toAffineLift_some, Point.fromAffine_some, negMap_of_Z_ne_zero, nonsingularLift_iff, negMap_of_Z_eq_zero, nonsingularLift_some, Point.toAffineLift_of_Z_ne_zero, addMap_of_Z_ne_zero, addMap_of_Z_eq_zero_right, nonsingularLift_zero, addMap_of_Z_eq_zero_left, Point.zero_point, Point.zero_def, Point.toAffineLift_eq, smul_eq, addMap_eq, negMap_eq, Point.toAffineLift_of_Z_eq_zero, addMap_of_Y_eq
instSMulForallFinOfNatNat 📖	CompOp	44 math math: addXYZ_of_Z_ne_zero, add_of_Y_ne', addZ_smul, addXYZ_of_X_eq, add_of_Y_eq, smul_fin3, addY_smul, dblZ_smul, add_smul_of_not_equiv, dblXYZ_of_Z_ne_zero, add_smul_equiv, dblY_smul, dblX_smul, addXYZ_smul, negDblY_smul, negAddY_smul, addXYZ_of_Z_eq_zero_right, addXYZ_neg, nonsingular_smul, add_of_Z_eq_zero_left, add_of_X_ne, Point.toAffine_smul, addX_smul, dblXYZ_of_Z_eq_zero, dblU_smul, negY_smul, smul_fin3_ext, equation_smul, dblXYZ_smul, addU_smul, smul_eq, neg_of_Z_ne_zero, comp_smul, smul_equiv_smul, add_of_Z_eq_zero_right, dblXYZ_of_Y_eq, addXYZ_of_Z_eq_zero_left, add_of_Z_eq_zero, smul_equiv, neg_smul, add_smul_of_equiv, neg_smul_equiv, neg_of_Z_eq_zero, add_of_Y_ne
instSetoidForallFinOfNatNat 📖	CompOp	17 math math: not_equiv_of_Y_ne, comp_equiv_comp, equiv_zero_of_Z_eq_zero, add_smul_equiv, equiv_iff_eq_of_Z_eq, neg_equiv, add_equiv, not_equiv_of_X_ne, equiv_iff_eq_of_Z_eq', equiv_of_X_eq_of_Y_eq, not_equiv_of_Z_eq_zero_left, smul_equiv_smul, not_equiv_of_Z_eq_zero_right, equiv_of_Z_eq_zero, equiv_some_of_Z_ne_zero, smul_equiv, neg_smul_equiv
polynomial 📖	CompOp	5 math math: polynomial_relation, baseChange_polynomial, eval_polynomial, map_polynomial, eval_polynomial_of_Z_ne_zero
polynomialX 📖	CompOp	6 math math: eval_polynomialX_of_Z_ne_zero, eval_polynomialX, polynomial_relation, baseChange_polynomialX, polynomialX_eq, map_polynomialX
polynomialY 📖	CompOp	6 math math: eval_polynomialY, polynomialY_eq, eval_polynomialY_of_Z_ne_zero, polynomial_relation, baseChange_polynomialY, map_polynomialY
polynomialZ 📖	CompOp	5 math math: baseChange_polynomialZ, polynomial_relation, polynomialZ_eq, map_polynomialZ, eval_polynomialZ
toAffine 📖	CompOp	40 math math: addXYZ_of_Z_ne_zero, Point.toAffineLift_neg, Point.toAffine_of_Z_eq_zero, add_of_Y_ne', Point.toAffineLift_some, dblX_of_Z_ne_zero, Point.toAffine_of_Z_ne_zero, negY_of_Z_ne_zero, Point.fromAffine_some, eval_polynomialX_of_Z_ne_zero, Point.toAffine_neg, negMap_of_Z_ne_zero, eval_polynomialY_of_Z_ne_zero, dblXYZ_of_Z_ne_zero, addX_of_Z_ne_zero, nonsingularLift_some, Point.toAffineLift_of_Z_ne_zero, addY_of_Z_ne_zero, dblY_of_Z_ne_zero, addMap_of_Z_ne_zero, Point.toAffineLift_add, Point.toAffineAddEquiv_apply, Point.toAffine_add, Point.toAffine_some, add_of_X_ne, Y_eq_iff', negAddY_of_Z_ne_zero, eval_polynomial_of_Z_ne_zero, nonsingular_some, nonsingular_of_Z_ne_zero, Point.toAffineLift_zero, Point.toAffine_zero, negDblY_of_Z_ne_zero, equation_some, Point.toAffineAddEquiv_symm_apply, neg_of_Z_ne_zero, equation_of_Z_ne_zero, Point.toAffine_of_singular, Point.toAffineLift_of_Z_eq_zero, Point.fromAffine_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_eq_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_eq_div_iff pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
X_eq_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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_pf_right
X_ne_zero_of_Z_eq_zero 📖	—	Nonsingular MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero pow_eq_zero_iff isReduced_of_noZeroDivisors two_ne_zero nonsingular_of_Z_eq_zero equation_of_Z_eq_zero zero_pow OfNat.ofNat_ne_zero Nat.instCharZero MulZeroClass.zero_mul
Y_eq_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_eq_div_iff pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
Y_eq_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_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_pf_right
Y_ne_zero_of_Z_eq_zero 📖	—	Nonsingular MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	X_ne_zero_of_Z_eq_zero eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors Nat.instAtLeastTwoHAddOfNat zero_pow two_ne_zero equation_of_Z_eq_zero nonsingular_of_Z_eq_zero
Z_eq_zero_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
baseChange_equation 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Equation WeierstrassCurve.toJacobian WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_equation AlgHom.toRingHom_eq_coe WeierstrassCurve.map_baseChange
baseChange_nonsingular 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	Nonsingular WeierstrassCurve.toJacobian WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_nonsingular AlgHom.toRingHom_eq_coe WeierstrassCurve.map_baseChange
baseChange_polynomial 📖	mathematical	—	polynomial WeierstrassCurve.toJacobian WeierstrassCurve.baseChange DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map 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.toJacobian WeierstrassCurve.baseChange DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map 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.toJacobian WeierstrassCurve.baseChange DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomialY WeierstrassCurve.map_baseChange
baseChange_polynomialZ 📖	mathematical	—	polynomialZ WeierstrassCurve.toJacobian WeierstrassCurve.baseChange DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomialZ WeierstrassCurve.map_baseChange
comp_equiv_comp 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	equiv_of_Z_eq_zero map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Z_eq_zero_of_equiv equiv_of_X_eq_of_Y_eq map_ne_zero_iff map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass X_eq_of_equiv Y_eq_of_equiv comp_smul
comp_fin3 📖	mathematical	—	Matrix.vecCons Matrix.vecEmpty	—	FinVec.map_eq
comp_smul 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike instSMulForallFinOfNatNat	—	Fintype.complete comp_fin3 map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
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 eval_polynomial
equation_of_Z_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Equation Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	MulZeroClass.mul_zero add_zero zero_pow OfNat.ofNat_ne_zero Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
equation_of_Z_ne_zero 📖	mathematical	—	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Equation toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	equation_of_equiv equiv_some_of_Z_ne_zero equation_some
equation_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Equation	—	equation_smul Units.isUnit
equation_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Equation instSMulForallFinOfNatNat	—	equation_iff Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_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_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add smul_smul IsUnit.val_inv_mul one_smul
equation_some 📖	mathematical	—	Equation Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty WeierstrassCurve.Affine.Equation toAffine	—	mul_one one_pow
equation_zero 📖	mathematical	—	Equation Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	one_pow
equiv_iff_eq_of_Z_eq 📖	mathematical	—	instSetoidForallFinOfNatNat	—	equiv_iff_eq_of_Z_eq' mem_nonZeroDivisors_of_ne_zero
equiv_iff_eq_of_Z_eq' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	instSetoidForallFinOfNatNat	—	mul_cancel_right_mem_nonZeroDivisors one_mul one_smul
equiv_of_X_eq_of_Y_eq 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Units.val_div_eq_div_val div_pow mul_comm mul_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain fin3_def
equiv_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain	—	isUnit_X_of_Z_eq_zero isUnit_Y_of_Z_eq_zero Units.val_div_eq_div_val mul_pow div_pow MulZeroClass.mul_zero fin3_def Nat.instAtLeastTwoHAddOfNat pow_succ IsUnit.mul_div_cancel_left IsUnit.pow IsUnit.div_mul_cancel_left IsUnit.inv_mul_cancel_right
equiv_some_of_Z_ne_zero 📖	mathematical	—	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.vecCons DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	equiv_of_X_eq_of_Y_eq one_ne_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq div_self pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Mathlib.Tactic.LinearCombination.eq_rearrange Matrix.tail_cons Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul 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.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.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
equiv_zero_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	equiv_of_Z_eq_zero nonsingular_zero IsLocalRing.toNontrivial Field.instIsLocalRing
eval_polynomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval 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.eq_1 map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.eval_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.eval_C
eval_polynomialX 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval 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 polynomialX_eq MvPolynomial.C_mul map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.eval_C MvPolynomial.eval_X map_add AddMonoidHomClass.toAddHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
eval_polynomialX_of_Z_ne_zero 📖	mathematical	—	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval polynomialX EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.evalEval CommRing.toCommSemiring WeierstrassCurve.Affine.polynomialX toAffine	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq div_self pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Mathlib.Tactic.LinearCombination.eq_rearrange eval_polynomialX WeierstrassCurve.Affine.evalEval_polynomialX Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt 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.add_pf_zero_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Nat.cast_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
eval_polynomialY 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval 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₃ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat polynomialY_eq map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.eval_C MvPolynomial.eval_X map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
eval_polynomialY_of_Z_ne_zero 📖	mathematical	—	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval polynomialY EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.evalEval CommRing.toCommSemiring WeierstrassCurve.Affine.polynomialY toAffine	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq div_self pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Mathlib.Tactic.LinearCombination.eq_rearrange Nat.instAtLeastTwoHAddOfNat eval_polynomialY WeierstrassCurve.Affine.evalEval_polynomialY Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_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 Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
eval_polynomialZ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval polynomialZ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul WeierstrassCurve.a₁ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Nat.instAtLeastTwoHAddOfNat polynomialZ_eq MvPolynomial.C_mul map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.eval_C MvPolynomial.eval_X map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
eval_polynomial_of_Z_ne_zero 📖	mathematical	—	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval polynomial EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.evalEval CommRing.toCommSemiring WeierstrassCurve.Affine.polynomial toAffine	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq div_self pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Mathlib.Tactic.LinearCombination.eq_rearrange eval_polynomial WeierstrassCurve.Affine.evalEval_polynomial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_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.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Tactic.Ring.mul_one Nat.cast_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
fin3_def 📖	mathematical	—	Matrix.vecCons Matrix.vecEmpty	—	Fintype.complete
fin3_def_ext 📖	mathematical	—	Matrix.vecCons Matrix.vecEmpty	—	—
isUnit_X_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Ne.isUnit X_ne_zero_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain
isUnit_Y_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Ne.isUnit Y_ne_zero_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain
map_equation 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	Equation WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_polynomial MvPolynomial.eval_map 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.toJacobian WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_equation map_polynomialX MvPolynomial.eval_map map_ne_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_polynomialY map_polynomialZ
map_polynomial 📖	mathematical	—	polynomial WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.map_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MvPolynomial.map_C
map_polynomialX 📖	mathematical	—	polynomialX WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map	—	map_polynomial MvPolynomial.pderiv_map
map_polynomialY 📖	mathematical	—	polynomialY WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map	—	map_polynomial MvPolynomial.pderiv_map
map_polynomialZ 📖	mathematical	—	polynomialZ WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map	—	map_polynomial MvPolynomial.pderiv_map
nonsingularLift_iff 📖	mathematical	—	NonsingularLift MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction instMulActionForallFinOfNatNat Nonsingular	—	—
nonsingularLift_some 📖	mathematical	—	NonsingularLift MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction instMulActionForallFinOfNatNat Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty WeierstrassCurve.Affine.Nonsingular toAffine	—	nonsingular_some
nonsingularLift_zero 📖	mathematical	—	NonsingularLift MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction instMulActionForallFinOfNatNat Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	nonsingular_zero
nonsingular_iff 📖	mathematical	—	Nonsingular Equation	—	Nat.instAtLeastTwoHAddOfNat Nonsingular.eq_1 eval_polynomialX eval_polynomialY eval_polynomialZ
nonsingular_iff_of_Z_ne_zero 📖	mathematical	—	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain Equation	—	nonsingular_of_Z_ne_zero WeierstrassCurve.Affine.Nonsingular.eq_1 equation_of_Z_ne_zero eval_polynomialX_of_Z_ne_zero div_ne_zero_iff pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain eval_polynomialY_of_Z_ne_zero
nonsingular_of_Z_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Nonsingular Equation	—	Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero zero_pow OfNat.ofNat_ne_zero Nat.instCharZero add_zero zero_sub sub_zero
nonsingular_of_Z_ne_zero 📖	mathematical	—	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Nonsingular toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	nonsingular_of_equiv equiv_some_of_Z_ne_zero nonsingular_some
nonsingular_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Nonsingular	—	nonsingular_smul Units.isUnit
nonsingular_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Nonsingular instSMulForallFinOfNatNat	—	Nat.instAtLeastTwoHAddOfNat nonsingular_iff equation_smul Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr 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_pf_right Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Units.isUnit smul_smul IsUnit.val_inv_mul one_smul
nonsingular_some 📖	mathematical	—	Nonsingular Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty WeierstrassCurve.Affine.Nonsingular toAffine	—	Nat.instAtLeastTwoHAddOfNat one_pow mul_one Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero 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 Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
nonsingular_zero 📖	mathematical	—	Nonsingular Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	Nat.instAtLeastTwoHAddOfNat one_ne_zero NeZero.one Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
not_equiv_of_X_ne 📖	mathematical	—	instSetoidForallFinOfNatNat	—	X_eq_of_equiv
not_equiv_of_Y_ne 📖	mathematical	—	instSetoidForallFinOfNatNat	—	Y_eq_of_equiv
not_equiv_of_Z_eq_zero_left 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	instSetoidForallFinOfNatNat	—	Z_eq_zero_of_equiv
not_equiv_of_Z_eq_zero_right 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	instSetoidForallFinOfNatNat	—	Z_eq_zero_of_equiv
polynomialX_eq 📖	mathematical	—	polynomialX MvPolynomial CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.instMul CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C WeierstrassCurve.a₁ MvPolynomial.X Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Distrib.toMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₂ WeierstrassCurve.a₄	—	Nat.instAtLeastTwoHAddOfNat polynomialX.eq_1 polynomial.eq_1 map_sub Derivation.instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_of_ne one_ne_zero Fin.instNeZeroHAddNatOfNat_mathlib_1 MvPolynomial.pderiv_mul MvPolynomial.pderiv_C MvPolynomial.pderiv_X_self map_ofNat RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt 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.instAtLeastTwo
polynomialY_eq 📖	mathematical	—	polynomialY MvPolynomial CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat MvPolynomial.X WeierstrassCurve.a₁ WeierstrassCurve.a₃ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp.instAddMonoid	—	Nat.instAtLeastTwoHAddOfNat polynomialY.eq_1 polynomial.eq_1 map_sub Derivation.instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_self MvPolynomial.pderiv_mul MvPolynomial.pderiv_C MvPolynomial.pderiv_X_of_ne one_ne_zero Fin.instNeZeroHAddNatOfNat_mathlib_1 map_ofNat RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.instAtLeastTwo
polynomialZ_eq 📖	mathematical	—	polynomialZ MvPolynomial CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommRing.toRing Finsupp.instAddMonoid Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C WeierstrassCurve.a₁ MvPolynomial.X Distrib.toMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Nat.instAtLeastTwoHAddOfNat polynomialZ.eq_1 polynomial.eq_1 map_sub Derivation.instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_of_ne MvPolynomial.pderiv_mul MvPolynomial.pderiv_C MvPolynomial.pderiv_X_self map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_ofNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_lt 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.Meta.NormNum.instAtLeastTwo
polynomial_relation 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.eval polynomial Distrib.toAdd polynomialX polynomialY polynomialZ	—	Nat.instAtLeastTwoHAddOfNat eval_polynomial eval_polynomialX eval_polynomialY eval_polynomialZ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf 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_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.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add
smul_eq 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction instMulActionForallFinOfNatNat instSMulForallFinOfNatNat	—	Quotient.eq smul_equiv
smul_equiv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat instSMulForallFinOfNatNat	—	—
smul_equiv_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat instSMulForallFinOfNatNat	—	Quotient.eq_iff_equiv smul_eq
smul_fin3 📖	mathematical	—	instSMulForallFinOfNatNat Matrix.vecCons Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.vecEmpty	—	—
smul_fin3_ext 📖	mathematical	—	instSMulForallFinOfNatNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	—

WeierstrassCurve.Jacobian.Equation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	WeierstrassCurve.Jacobian.Equation WeierstrassCurve.toJacobian WeierstrassCurve.baseChange	WeierstrassCurve.Jacobian.Equation WeierstrassCurve.toJacobian 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.Jacobian.Equation	WeierstrassCurve.Jacobian.Equation WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	eq_1 WeierstrassCurve.Jacobian.map_polynomial MvPolynomial.eval_map MvPolynomial.eval₂_comp map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index