Basic

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

Statistics

Metric	Count
Definitions Equation, Nonsingular, NonsingularLift, PointClass, instSetoidForallFinOfNatNat, polynomial, polynomialX, polynomialY, polynomialZ, toAffine, toProjective	11
Theorems baseChange, map, X_eq_iff, X_eq_of_equiv, X_eq_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_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	71
Total	82

WeierstrassCurve

Definitions

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

WeierstrassCurve.Projective

Definitions

Name	Category	Theorems
Equation 📖	MathDef	15 math math: Equation.baseChange, nonsingular_iff, equation_of_Z_eq_zero, baseChange_equation, nonsingular_iff_of_Z_ne_zero, map_equation, equation_smul, Equation.map, nonsingular_of_Z_eq_zero, equation_iff, equation_zero, equation_of_equiv, equation_some, nonsingular_iff_of_Y_eq_negY, equation_of_Z_ne_zero
Nonsingular 📖	MathDef	18 math math: nonsingular_neg, nonsingular_of_Z_ne_zero, Point.toAffine_some, Point.toAffineLift_of_Z_ne_zero, Point.toAffineLift_some, nonsingular_iff, nonsingularLift_iff, nonsingular_add, nonsingular_iff_of_Z_ne_zero, Point.toAffine_of_Z_ne_zero, nonsingular_of_equiv, baseChange_nonsingular, nonsingular_some, nonsingular_zero, nonsingular_of_Z_eq_zero, nonsingular_iff_of_Y_eq_negY, map_nonsingular, nonsingular_smul
NonsingularLift 📖	MathDef	7 math math: nonsingularLift_some, Point.nonsingular, nonsingularLift_addMap, Point.fromAffine_some, nonsingularLift_iff, nonsingularLift_zero, nonsingularLift_negMap
PointClass 📖	CompOp	—
instSetoidForallFinOfNatNat 📖	CompOp	17 math math: not_equiv_of_Z_eq_zero_right, not_equiv_of_Z_eq_zero_left, comp_equiv_comp, equiv_some_of_Z_ne_zero, neg_equiv, smul_equiv_smul, add_equiv, equiv_iff_eq_of_Z_eq', equiv_of_Z_eq_zero, add_smul_equiv, equiv_iff_eq_of_Z_eq, equiv_zero_of_Z_eq_zero, equiv_of_X_eq_of_Y_eq, not_equiv_of_X_ne, neg_smul_equiv, not_equiv_of_Y_ne, smul_equiv
polynomial 📖	CompOp	5 math math: eval_polynomial, polynomial_relation, baseChange_polynomial, eval_polynomial_of_Z_ne_zero, map_polynomial
polynomialX 📖	CompOp	12 math math: polynomial_relation, eval_polynomialX, eval_polynomialX_of_Z_ne_zero, map_polynomialX, polynomialX_eq, negDblY_eq, baseChange_polynomialX, negDblY_eq', dblX_eq, dblX_eq', dblY_of_Y_eq', negDblY_of_Y_eq'
polynomialY 📖	CompOp	6 math math: polynomial_relation, baseChange_polynomialY, polynomialY_eq, eval_polynomialY_of_Z_ne_zero, map_polynomialY, eval_polynomialY
polynomialZ 📖	CompOp	5 math math: polynomial_relation, polynomialZ_eq, eval_polynomialZ, map_polynomialZ, baseChange_polynomialZ
toAffine 📖	CompOp	40 math math: nonsingularLift_some, Y_eq_iff', nonsingular_of_Z_ne_zero, Point.toAffine_some, Point.toAffineLift_of_Z_ne_zero, Point.toAffineAddEquiv_apply, addY_of_Z_ne_zero, Point.toAffineLift_neg, Point.toAffineLift_zero, Point.toAffineLift_of_Z_eq_zero, Point.toAffineLift_some, negY_of_Z_ne_zero, Point.toAffine_of_singular, eval_polynomialX_of_Z_ne_zero, addXYZ_of_Z_ne_zero, negDblY_of_Z_ne_zero, Point.toAffine_neg, Point.fromAffine_some, negMap_of_Z_ne_zero, neg_of_Z_ne_zero, eval_polynomialY_of_Z_ne_zero, dblXYZ_of_Z_ne_zero, Point.toAffine_of_Z_ne_zero, dblY_of_Z_ne_zero, Point.toAffineLift_add, add_of_X_ne, eval_polynomial_of_Z_ne_zero, add_of_Y_ne', addMap_of_Z_ne_zero, Point.toAffine_add, nonsingular_some, Point.toAffine_of_Z_eq_zero, Point.toAffine_zero, Point.fromAffine_zero, addX_of_Z_ne_zero, Point.toAffineAddEquiv_symm_apply, negAddY_of_Z_ne_zero, dblX_of_Z_ne_zero, equation_some, equation_of_Z_ne_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 DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_eq_div_iff
X_eq_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Ring.of_eq 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
X_eq_zero_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors equation_of_Z_eq_zero
Y_eq_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_eq_div_iff
Y_eq_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Ring.of_eq 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
Y_ne_zero_of_Z_eq_zero 📖	—	Nonsingular MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	Nat.instAtLeastTwoHAddOfNat nonsingular_of_Z_eq_zero X_eq_zero_of_Z_eq_zero zero_pow two_ne_zero MulZeroClass.mul_zero add_zero sub_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.toProjective 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.toProjective 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.toProjective 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.toProjective 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.toProjective 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.toProjective 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 X_eq_of_equiv Y_eq_of_equiv MonoidWithZeroHomClass.toMonoidHomClass 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 Function.hasSMul Algebra.toSMul Algebra.id	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
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 Distrib.toMul Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Equation.eq_1 eval_polynomial sub_eq_zero
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.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MulZeroClass.mul_zero add_zero zero_pow OfNat.ofNat_ne_zero Nat.instCharZero Nat.instAtLeastTwoHAddOfNat zero_sub
equation_of_Z_ne_zero 📖	mathematical	—	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Equation toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	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 Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	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.mul_congr Mathlib.Tactic.Ring.pow_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.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_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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 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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty	—	zero_pow three_ne_zero
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	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Units.val_div_eq_div_val smul_fin3 mul_comm mul_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass 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_Y_of_Z_eq_zero Units.val_div_eq_div_val smul_fin3 X_eq_zero_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain MulZeroClass.mul_zero IsUnit.div_mul_cancel fin3_def
equiv_some_of_Z_ne_zero 📖	mathematical	—	instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.vecCons DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing 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 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.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.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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing 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 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 Distrib.toMul Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	polynomial.eq_1 map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.eval_X 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.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 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_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 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul WeierstrassCurve.a₁ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Nat.instAtLeastTwoHAddOfNat polynomialZ_eq MvPolynomial.C_mul 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_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.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 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 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.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_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.toProjective 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.toProjective 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.toProjective 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_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.map_X MvPolynomial.map_C
map_polynomialX 📖	mathematical	—	polynomialX WeierstrassCurve.toProjective 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.toProjective 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.toProjective 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 Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Nonsingular	—	—
nonsingularLift_some 📖	mathematical	—	NonsingularLift MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule 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 Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing 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 add_zero zero_pow OfNat.ofNat_ne_zero Nat.instCharZero zero_sub
nonsingular_of_Z_ne_zero 📖	mathematical	—	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Nonsingular toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	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 Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw 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.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.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.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.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.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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty	—	Nat.instAtLeastTwoHAddOfNat one_ne_zero NeZero.one Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd 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.add_pf_add_zero 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero 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.Meta.NormNum.IsNat.of_raw 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_mul MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_of_ne one_ne_zero Fin.instNeZeroHAddNatOfNat_mathlib_1 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 Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Nat.cast_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.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_mul MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_self MvPolynomial.pderiv_X_of_ne MvPolynomial.pderiv_C 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.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow 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.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 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring MvPolynomial.X AddMonoidAlgebra.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C WeierstrassCurve.a₁ Distrib.toMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Nat.instAtLeastTwoHAddOfNat polynomialZ.eq_1 polynomial.eq_1 map_sub Derivation.instAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass MvPolynomial.pderiv_mul MvPolynomial.pderiv_pow MvPolynomial.pderiv_X_of_ne MvPolynomial.pderiv_X_self MvPolynomial.pderiv_C 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 Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Nat.cast_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.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.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.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add 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 Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Function.hasSMul Algebra.toSMul Algebra.id	—	Quotient.eq smul_equiv
smul_equiv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	—
smul_equiv_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	Quotient.eq_iff_equiv smul_eq
smul_fin3 📖	mathematical	—	Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Matrix.vecCons Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	Matrix.cons_val_succ Matrix.cons_val_fin_one
smul_fin3_ext 📖	mathematical	—	Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

WeierstrassCurve.Projective.Equation

Theorems

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

---

← Back to Index