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	38 math math: Jacobian.map_addX, 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.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	13 math math: nonsingular_iff_of_Y_eq_negY, map_equation, equation_of_equiv, baseChange_equation, nonsingular_of_Z_eq_zero, equation_iff, equation_of_Z_eq_zero, equation_smul, equation_zero, equation_some, equation_of_Z_ne_zero, nonsingular_iff, nonsingular_iff_of_Z_ne_zero
Nonsingular 📖	MathDef	14 math math: nonsingular_iff_of_Y_eq_negY, Point.toAffineLift_some, nonsingularLift_iff, baseChange_nonsingular, Point.toAffineLift_of_Z_ne_zero, nonsingular_of_Z_eq_zero, map_nonsingular, nonsingular_smul, nonsingular_some, nonsingular_of_Z_ne_zero, nonsingular_zero, nonsingular_of_equiv, nonsingular_iff, nonsingular_iff_of_Z_ne_zero
NonsingularLift 📖	MathDef	5 math math: Point.nonsingular, Point.fromAffine_some, nonsingularLift_iff, nonsingularLift_some, nonsingularLift_zero
PointClass 📖	CompOp	—
instMulActionForallFinOfNatNat 📖	CompOp	15 math math: Point.fromAffine_some, negMap_of_Z_ne_zero, nonsingularLift_iff, negMap_of_Z_eq_zero, nonsingularLift_some, 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, smul_eq, addMap_eq, negMap_eq, 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	15 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, 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	39 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, 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.toNatPow 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.toNatPow 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.toNatPow 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.toNatPow 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	—	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	—	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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_polynomialZ WeierstrassCurve.map_baseChange
comp_equiv_comp 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	instSetoidForallFinOfNatNat 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.toNatPow 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.toNatPow 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.toNatPow 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.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	instSetoidForallFinOfNatNat	—	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	—	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.toNatPow 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 Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	equiv_of_Z_eq_zero nonsingular_zero IsLocalRing.toNontrivial Field.instIsLocalRing
eval_polynomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialY EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomial EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow 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	—	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	—	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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map	—	map_polynomial MvPolynomial.pderiv_map
map_polynomialY 📖	mathematical	—	polynomialY WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map	—	map_polynomial MvPolynomial.pderiv_map
map_polynomialZ 📖	mathematical	—	polynomialZ WeierstrassCurve.toJacobian WeierstrassCurve.map DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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.toNatPow 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 CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C WeierstrassCurve.a₁ MvPolynomial.X Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat MvPolynomial.X WeierstrassCurve.a₁ WeierstrassCurve.a₃ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	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 CommRing.toRing MvPolynomial.instCommRingMvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.C WeierstrassCurve.a₁ MvPolynomial.X instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring 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 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.toNatPow 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.toNatPow 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	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.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