Formula

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

Statistics

Metric	Count
Definitions Formula, addU, addX, addXYZ, addY, addZ, dblU, dblX, dblXYZ, dblY, dblZ, negAddY, negDblY, negY	14
Theorems Y_eq_iff', Y_eq_negY_of_Y_eq, Y_eq_of_Y_ne, Y_eq_of_Y_ne', Y_ne_negY_of_Y_ne, Y_ne_negY_of_Y_ne', Y_sub_Y_add_Y_sub_negY, Y_sub_Y_mul_Y_sub_negY, addU_ne_zero_of_Y_ne, addU_of_Z_eq_zero_left, addU_of_Z_eq_zero_right, addU_smul, addXYZ_X, addXYZ_Y, addXYZ_Z, addXYZ_of_X_eq, addXYZ_of_Z_eq_zero_left, addXYZ_of_Z_eq_zero_right, addXYZ_of_Z_ne_zero, addXYZ_self, addXYZ_smul, addX_eq, addX_eq', addX_of_X_eq, addX_of_Z_eq_zero_left, addX_of_Z_eq_zero_right, addX_of_Z_ne_zero, addX_self, addX_smul, addY_of_X_eq, addY_of_X_eq', addY_of_Z_eq_zero_left, addY_of_Z_eq_zero_right, addY_of_Z_ne_zero, addY_self, addY_smul, addZ_eq, addZ_eq', addZ_ne_zero_of_X_ne, addZ_of_X_eq, addZ_of_Z_eq_zero_left, addZ_of_Z_eq_zero_right, addZ_self, addZ_smul, baseChange_addX, baseChange_addXYZ, baseChange_addY, baseChange_dblU, baseChange_dblX, baseChange_dblXYZ, baseChange_dblY, baseChange_dblZ, baseChange_negAddY, baseChange_negDblY, baseChange_negY, dblU_eq, dblU_ne_zero_of_Y_eq, dblU_of_Z_eq_zero, dblU_smul, dblXYZ_X, dblXYZ_Y, dblXYZ_Z, dblXYZ_of_Y_eq, dblXYZ_of_Z_eq_zero, dblXYZ_of_Z_ne_zero, dblXYZ_smul, dblX_eq, dblX_eq', dblX_of_Y_eq, dblX_of_Z_eq_zero, dblX_of_Z_ne_zero, dblX_smul, dblY_of_Y_eq, dblY_of_Y_eq', dblY_of_Z_eq_zero, dblY_of_Z_ne_zero, dblY_smul, dblZ_ne_zero_of_Y_ne, dblZ_ne_zero_of_Y_ne', dblZ_of_Y_eq, dblZ_of_Z_eq_zero, dblZ_smul, isUnit_addU_of_Y_ne, isUnit_addZ_of_X_ne, isUnit_dblU_of_Y_eq, isUnit_dblZ_of_Y_ne, isUnit_dblZ_of_Y_ne', map_addU, map_addX, map_addXYZ, map_addY, map_addZ, map_dblU, map_dblX, map_dblXYZ, map_dblY, map_dblZ, map_negAddY, map_negDblY, map_negY, negAddY_eq, negAddY_eq', negAddY_of_X_eq, negAddY_of_X_eq', negAddY_of_Z_eq_zero_left, negAddY_of_Z_eq_zero_right, negAddY_of_Z_ne_zero, negAddY_self, negAddY_smul, negDblY_eq, negDblY_eq', negDblY_of_Y_eq, negDblY_of_Y_eq', negDblY_of_Z_eq_zero, negDblY_of_Z_ne_zero, negDblY_smul, negY_eq, negY_of_Z_eq_zero, negY_of_Z_ne_zero, negY_smul, nonsingular_iff_of_Y_eq_negY	121
Total	135

FirstOrder.Language

Definitions

Name	Category	Theorems
Formula 📖	CompOp	23 math math: Theory.CompleteType.compl_setOf_mem, Theory.CompleteType.mem_or_not_mem, Formula.realize_bot, BoundedFormula.instCountableFormula, Formula.equivSentence_not, Theory.IsMaximal.mem_or_not_mem, LEquiv.onFormula_apply, Formula.inf_iff_not_sup_not, Formula.equivSentence_inf, Theory.models_formula_iff_onTheory_models_equivSentence, Formula.realize_equivSentence_symm_con, Theory.CompleteType.formula_mem_typeOf, LEquiv.onFormula_symm, completeTheory.mem_or_not_mem, Theory.CompleteType.not_mem_iff, Formula.realize_sup, Theory.CompleteType.mem_typeOf, Formula.realize_inf, Formula.realize_top, Formula.sup_iff_not_inf_not, Formula.realize_equivSentence_symm, Formula.realize_equivSentence, Theory.models_iff_not_satisfiable

WeierstrassCurve.Projective

Definitions

Name	Category	Theorems
addU 📖	CompOp	9 math math: addY_of_X_eq, negAddY_of_X_eq, addXYZ_of_X_eq, isUnit_addU_of_Y_ne, addU_of_Z_eq_zero_left, addU_smul, map_addU, add_of_Y_ne, addU_of_Z_eq_zero_right
addX 📖	CompOp	12 math math: addX_smul, addX_of_X_eq, addX_neg, addX_of_Z_eq_zero_left, addX_eq, baseChange_addX, addXYZ_X, addX_eq', map_addX, addX_of_Z_ne_zero, addX_of_Z_eq_zero_right, addX_self
addXYZ 📖	CompOp	13 math math: addXYZ_smul, addXYZ_of_X_eq, baseChange_addXYZ, addXYZ_neg, addXYZ_of_Z_eq_zero_left, addXYZ_of_Z_ne_zero, addXYZ_of_Z_eq_zero_right, map_addXYZ, addXYZ_X, addXYZ_Z, add_of_not_equiv, addXYZ_Y, addXYZ_self
addY 📖	CompOp	11 math math: addY_neg, addY_smul, addY_of_X_eq', addY_of_X_eq, addY_of_Z_ne_zero, addY_of_Z_eq_zero_left, map_addY, addY_of_Z_eq_zero_right, addY_self, addXYZ_Y, baseChange_addY
addZ 📖	CompOp	16 math math: addY_of_Z_ne_zero, addZ_smul, addXYZ_of_Z_ne_zero, addZ_eq, addZ_of_Z_eq_zero_right, addZ_eq', addZ_of_Z_eq_zero_left, addZ_self, add_of_X_ne, addXYZ_Z, map_addZ, addZ_neg, addX_of_Z_ne_zero, negAddY_of_Z_ne_zero, isUnit_addZ_of_X_ne, addZ_of_X_eq
dblU 📖	CompOp	10 math math: dblU_smul, dblU_eq, dblU_of_Z_eq_zero, isUnit_dblU_of_Y_eq, map_dblU, add_of_Y_eq, baseChange_dblU, dblY_of_Y_eq, dblXYZ_of_Y_eq, negDblY_of_Y_eq
dblX 📖	CompOp	9 math math: dblX_smul, baseChange_dblX, dblX_of_Z_eq_zero, dblX_of_Y_eq, dblX_eq, dblXYZ_X, dblX_eq', dblX_of_Z_ne_zero, map_dblX
dblXYZ 📖	CompOp	12 math math: dblXYZ_smul, baseChange_dblXYZ, dblXYZ_Z, dblXYZ_of_Z_eq_zero, add_of_equiv, add_self, dblXYZ_of_Z_ne_zero, map_dblXYZ, add_of_eq, dblXYZ_X, dblXYZ_of_Y_eq, dblXYZ_Y
dblY 📖	CompOp	8 math math: map_dblY, dblY_of_Z_ne_zero, dblY_smul, dblY_of_Z_eq_zero, baseChange_dblY, dblY_of_Y_eq', dblY_of_Y_eq, dblXYZ_Y
dblZ 📖	CompOp	16 math math: map_dblZ, addY_neg, dblZ_of_Z_eq_zero, addXYZ_neg, dblXYZ_Z, isUnit_dblZ_of_Y_ne, negAddY_neg, negDblY_of_Z_ne_zero, baseChange_dblZ, dblXYZ_of_Z_ne_zero, isUnit_dblZ_of_Y_ne', dblZ_of_Y_eq, dblY_of_Z_ne_zero, add_of_Y_ne', dblX_of_Z_ne_zero, dblZ_smul
negAddY 📖	CompOp	12 math math: map_negAddY, baseChange_negAddY, negAddY_self, negAddY_of_X_eq, negAddY_eq', negAddY_smul, negAddY_of_X_eq', negAddY_neg, negAddY_of_Z_eq_zero_right, negAddY_eq, negAddY_of_Z_ne_zero, negAddY_of_Z_eq_zero_left
negDblY 📖	CompOp	9 math math: baseChange_negDblY, map_negDblY, negDblY_of_Z_eq_zero, negDblY_of_Z_ne_zero, negDblY_eq, negDblY_smul, negDblY_eq', negDblY_of_Y_eq, negDblY_of_Y_eq'
negY 📖	CompOp	17 math math: negY_eq, negY_of_Z_eq_zero, Y_eq_iff', baseChange_negY, neg_Y, Y_sub_Y_mul_Y_sub_negY, negY_of_Z_ne_zero, negY_smul, negDblY_eq, negAddY_of_Z_eq_zero_right, negDblY_eq', dblX_eq, dblX_eq', negAddY_of_Z_eq_zero_left, map_negY, Y_eq_of_Y_ne, Y_sub_Y_add_Y_sub_negY

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Y_eq_iff' 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain negY DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.negY toAffine	—	div_eq_div_iff negY_of_Z_ne_zero
Y_eq_negY_of_Y_eq 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	—	—	mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero NoZeroDivisors.to_isCancelMulZero Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Y_sub_Y_add_Y_sub_negY 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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq 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.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
Y_eq_of_Y_ne 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negY	—	sub_eq_zero mul_eq_zero Y_sub_Y_mul_Y_sub_negY mul_ne_zero sub_ne_zero
Y_eq_of_Y_ne' 📖	—	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	sub_eq_zero mul_eq_zero Y_sub_Y_mul_Y_sub_negY sub_ne_zero mul_ne_zero
Y_ne_negY_of_Y_ne 📖	—	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	sub_eq_zero Y_eq_of_Y_ne Mathlib.Tactic.Contrapose.contrapose₄ Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Y_sub_Y_add_Y_sub_negY 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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
Y_ne_negY_of_Y_ne' 📖	—	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	sub_eq_zero Y_eq_of_Y_ne' Mathlib.Tactic.Contrapose.contrapose₄ Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Y_sub_Y_add_Y_sub_negY 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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt
Y_sub_Y_add_Y_sub_negY 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Distrib.toAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing negY	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange negY.eq_1 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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
Y_sub_Y_mul_Y_sub_negY 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing negY MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange negY.eq_1 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.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_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one 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 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_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
addU_ne_zero_of_Y_ne 📖	—	—	—	—	div_ne_zero neg_ne_zero pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain sub_ne_zero mul_ne_zero
addU_of_Z_eq_zero_left 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	addU	—	addU.eq_1 MulZeroClass.zero_mul div_zero
addU_of_Z_eq_zero_right 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	addU	—	addU.eq_1 MulZeroClass.mul_zero div_zero
addU_smul 📖	mathematical	—	addU Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id 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	—	Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.zpow'_ofNat one_ne_zero NeZero.one GroupWithZero.toNontrivial
addXYZ_X 📖	mathematical	—	addXYZ addX	—	—
addXYZ_Y 📖	mathematical	—	addXYZ addY	—	—
addXYZ_Z 📖	mathematical	—	addXYZ addZ	—	—
addXYZ_of_X_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addXYZ Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id addU Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	addXYZ.eq_1 addX_of_X_eq IsDomain.to_noZeroDivisors instIsDomain addY_of_X_eq addZ_of_X_eq smul_fin3 MulZeroClass.mul_zero mul_one
addXYZ_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addXYZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	addXYZ.eq_1 addX_of_Z_eq_zero_left addY_of_Z_eq_zero_left addZ_of_Z_eq_zero_left smul_fin3
addXYZ_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addXYZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	addXYZ.eq_1 addX_of_Z_eq_zero_right addY_of_Z_eq_zero_right addZ_of_Z_eq_zero_right smul_fin3
addXYZ_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	addXYZ Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id addZ Matrix.vecCons WeierstrassCurve.Affine.addX toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	isUnit_addZ_of_X_ne addXYZ.eq_1 smul_fin3 addX_of_Z_ne_zero IsUnit.mul_div_cancel addY_of_Z_ne_zero mul_one
addXYZ_self 📖	mathematical	—	addXYZ Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.vecEmpty	—	addXYZ.eq_1 addX_self addY_self addZ_self
addXYZ_smul 📖	mathematical	—	addXYZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addXYZ.eq_1 addX_smul addY_smul addZ_smul smul_fin3 addXYZ_X addXYZ_Y addXYZ_Z
addX_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	addX DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Distrib.toAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WeierstrassCurve.a₁ WeierstrassCurve.a₂	—	addX_eq' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain mul_ne_zero
addX_eq' 📖	mathematical	Equation	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing addX Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd WeierstrassCurve.a₁ WeierstrassCurve.a₂	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange addX.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.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_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
addX_of_X_eq 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addX MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	eq_zero_of_ne_zero_of_mul_right_eq_zero pow_ne_zero isReduced_of_noZeroDivisors mul_ne_zero addX_eq' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_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_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
addX_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addX Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addX.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos
addX_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addX Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addX.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.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_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos
addX_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing addX addZ WeierstrassCurve.Affine.addX toAffine WeierstrassCurve.Affine.slope	—	addX_eq addZ_eq sub_ne_zero
addX_self 📖	mathematical	—	addX MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addX.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.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_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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
addX_smul 📖	mathematical	—	addX Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_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.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.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_pow Mathlib.Tactic.Ring.pow_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.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
addY_of_X_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addY addU	—	addU.eq_1 mul_div_mul_right pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain mul_ne_zero addY_of_X_eq' pow_succ' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass
addY_of_X_eq' 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq negAddY_of_X_eq' Mathlib.Tactic.LinearCombination.eq_rearrange addY.eq_1 negY_eq addX_of_X_eq addZ_of_X_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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 Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_congr 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.cast_pos 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.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
addY_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addY Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addY.eq_1 negY_eq negAddY_of_Z_eq_zero_left negY.eq_1 addX_of_Z_eq_zero_left addZ_of_Z_eq_zero_left Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add 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
addY_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addY Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addY.eq_1 negY_eq negAddY_of_Z_eq_zero_right negY.eq_1 addX_of_Z_eq_zero_right addZ_of_Z_eq_zero_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
addY_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing addY addZ WeierstrassCurve.Affine.addY toAffine WeierstrassCurve.Affine.slope	—	addY.eq_1 negY_of_Z_ne_zero addZ_ne_zero_of_X_ne IsDomain.to_noZeroDivisors instIsDomain addX_of_Z_ne_zero negAddY_of_Z_ne_zero WeierstrassCurve.Affine.addY.eq_1
addY_self 📖	mathematical	—	addY MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addX_self negAddY_self addZ_self neg_zero MulZeroClass.mul_zero sub_zero
addY_smul 📖	mathematical	—	addY Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	addX_smul negAddY_smul addZ_smul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
addZ_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	addZ DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addZ_eq' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain
addZ_eq' 📖	mathematical	Equation	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing addZ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange addZ.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.mul_one 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_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_zero Nat.cast_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.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf
addZ_ne_zero_of_X_ne 📖	—	Equation	—	—	left_ne_zero_of_mul addZ_eq' pow_ne_zero isReduced_of_noZeroDivisors sub_ne_zero
addZ_of_X_eq 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addZ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	eq_zero_of_ne_zero_of_mul_right_eq_zero mul_ne_zero addZ_eq' sub_self zero_pow three_ne_zero
addZ_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addZ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addZ.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
addZ_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addZ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	addZ.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero 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_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
addZ_self 📖	mathematical	—	addZ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addZ.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.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_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.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
addZ_smul 📖	mathematical	—	addZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq 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_mul
baseChange_addX 📖	mathematical	—	addX WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addX WeierstrassCurve.map_baseChange
baseChange_addXYZ 📖	mathematical	—	addXYZ WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addXYZ WeierstrassCurve.map_baseChange
baseChange_addY 📖	mathematical	—	addY WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addY WeierstrassCurve.map_baseChange
baseChange_dblU 📖	mathematical	—	dblU WeierstrassCurve.toProjective WeierstrassCurve.baseChange EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe AlgHom CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_dblU WeierstrassCurve.map_baseChange
baseChange_dblX 📖	mathematical	—	dblX WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_dblX WeierstrassCurve.map_baseChange
baseChange_dblXYZ 📖	mathematical	—	dblXYZ WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_dblXYZ WeierstrassCurve.map_baseChange
baseChange_dblY 📖	mathematical	—	dblY WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_dblY WeierstrassCurve.map_baseChange
baseChange_dblZ 📖	mathematical	—	dblZ WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_dblZ WeierstrassCurve.map_baseChange
baseChange_negAddY 📖	mathematical	—	negAddY WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_negAddY WeierstrassCurve.map_baseChange
baseChange_negDblY 📖	mathematical	—	negDblY WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_negDblY WeierstrassCurve.map_baseChange
baseChange_negY 📖	mathematical	—	negY WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_negY WeierstrassCurve.map_baseChange
dblU_eq 📖	mathematical	—	dblU DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.a₁ Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₂ WeierstrassCurve.a₄	—	Nat.instAtLeastTwoHAddOfNat dblU.eq_1 eval_polynomialX
dblU_ne_zero_of_Y_eq 📖	—	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	—	—	div_ne_zero pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain nonsingular_iff_of_Y_eq_negY Y_eq_negY_of_Y_eq
dblU_of_Z_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	dblU	—	Nat.instAtLeastTwoHAddOfNat dblU_eq zero_pow two_ne_zero div_zero
dblU_smul 📖	mathematical	—	dblU Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id 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	—	Nat.instAtLeastTwoHAddOfNat dblU_eq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' one_ne_zero NeZero.one GroupWithZero.toNontrivial
dblXYZ_X 📖	mathematical	—	dblXYZ dblX	—	—
dblXYZ_Y 📖	mathematical	—	dblXYZ dblY	—	—
dblXYZ_Z 📖	mathematical	—	dblXYZ dblZ	—	—
dblXYZ_of_Y_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	dblXYZ Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id dblU Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	dblXYZ.eq_1 dblX_of_Y_eq IsDomain.to_noZeroDivisors instIsDomain dblY_of_Y_eq dblZ_of_Y_eq smul_fin3 MulZeroClass.mul_zero mul_one
dblXYZ_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	dblXYZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty	—	dblXYZ.eq_1 dblX_of_Z_eq_zero dblY_of_Z_eq_zero dblZ_of_Z_eq_zero smul_fin3 MulZeroClass.mul_zero mul_one
dblXYZ_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	dblXYZ Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id dblZ Matrix.vecCons WeierstrassCurve.Affine.addX toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	isUnit_dblZ_of_Y_ne' dblXYZ.eq_1 smul_fin3 dblX_of_Z_ne_zero IsUnit.mul_div_cancel dblY_of_Z_ne_zero mul_one
dblXYZ_smul 📖	mathematical	—	dblXYZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	dblXYZ.eq_1 dblX_smul dblY_smul dblZ_smul smul_fin3 dblXYZ_X dblXYZ_Y dblXYZ_Z
dblX_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	dblX DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX WeierstrassCurve.a₁ negY WeierstrassCurve.a₂ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat dblX_eq' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass
dblX_eq' 📖	mathematical	Equation	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing dblX SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX WeierstrassCurve.a₁ negY WeierstrassCurve.a₂ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange dblX.eq_1 eval_polynomialX negY.eq_1 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_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.pow_congr 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.mul_pf_left 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.add_pf_add_gt 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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
dblX_of_Y_eq 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	dblX MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	eq_zero_of_ne_zero_of_mul_right_eq_zero Nat.instAtLeastTwoHAddOfNat dblX_eq' Y_eq_negY_of_Y_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_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.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_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.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
dblX_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	dblX	—	dblX.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add 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.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
dblX_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing dblX dblZ WeierstrassCurve.Affine.addX toAffine WeierstrassCurve.Affine.slope	—	Nat.instAtLeastTwoHAddOfNat dblX_eq dblZ.eq_1 X_eq_iff sub_ne_zero Y_ne_negY_of_Y_ne' IsDomain.to_noZeroDivisors instIsDomain
dblX_smul 📖	mathematical	—	dblX Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_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_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_one 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_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_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.add_pf_add_gt
dblY_of_Y_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	dblY dblU	—	dblU.eq_1 dblY_of_Y_eq' IsDomain.to_noZeroDivisors instIsDomain mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors
dblY_of_Y_eq' 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	dblY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd negDblY_of_Y_eq' Mathlib.Tactic.LinearCombination.eq_rearrange dblY.eq_1 negY_eq dblX_of_Y_eq dblZ_of_Y_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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 Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos 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.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right 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
dblY_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	dblY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	dblY.eq_1 negY_eq negDblY_of_Z_eq_zero dblX_of_Z_eq_zero dblZ_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf
dblY_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing dblY dblZ WeierstrassCurve.Affine.addY toAffine WeierstrassCurve.Affine.slope	—	dblY.eq_1 negY_of_Z_ne_zero dblZ_ne_zero_of_Y_ne' IsDomain.to_noZeroDivisors instIsDomain dblX_of_Z_ne_zero negDblY_of_Z_ne_zero WeierstrassCurve.Affine.addY.eq_1
dblY_smul 📖	mathematical	—	dblY Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	dblX_smul negDblY_smul dblZ_smul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
dblZ_ne_zero_of_Y_ne 📖	—	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	mul_ne_zero pow_ne_zero isReduced_of_noZeroDivisors sub_ne_zero Y_ne_negY_of_Y_ne
dblZ_ne_zero_of_Y_ne' 📖	—	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	mul_ne_zero pow_ne_zero isReduced_of_noZeroDivisors sub_ne_zero Y_ne_negY_of_Y_ne'
dblZ_of_Y_eq 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	dblZ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	dblZ.eq_1 Y_eq_negY_of_Y_eq sub_self zero_pow three_ne_zero MulZeroClass.mul_zero
dblZ_of_Z_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	dblZ	—	dblZ.eq_1 MulZeroClass.zero_mul
dblZ_smul 📖	mathematical	—	dblZ Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	negY_smul 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 Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.pow_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_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow
isUnit_addU_of_Y_ne 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addU	—	Ne.isUnit addU_ne_zero_of_Y_ne
isUnit_addZ_of_X_ne 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield addZ	—	Ne.isUnit addZ_ne_zero_of_X_ne IsDomain.to_noZeroDivisors instIsDomain
isUnit_dblU_of_Y_eq 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield dblU	—	Ne.isUnit dblU_ne_zero_of_Y_eq
isUnit_dblZ_of_Y_ne 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield dblZ	—	Ne.isUnit dblZ_ne_zero_of_Y_ne IsDomain.to_noZeroDivisors instIsDomain
isUnit_dblZ_of_Y_ne' 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield dblZ	—	Ne.isUnit dblZ_ne_zero_of_Y_ne' IsDomain.to_noZeroDivisors instIsDomain
map_addU 📖	mathematical	—	addU DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_neg RingHomClass.toAddMonoidHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass map_sub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
map_addX 📖	mathematical	—	addX WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_ofNat
map_addXYZ 📖	mathematical	—	addXYZ WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_addX map_addY map_addZ comp_fin3
map_addY 📖	mathematical	—	addY WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_addX map_negAddY map_addZ map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_neg map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
map_addZ 📖	mathematical	—	addZ WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_sub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_neg map_ofNat map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_dblU 📖	mathematical	—	dblU WeierstrassCurve.toProjective WeierstrassCurve.map EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	Nat.instAtLeastTwoHAddOfNat dblU_eq map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass map_sub RingHomClass.toAddMonoidHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_add AddMonoidHomClass.toAddHomClass map_ofNat
map_dblX 📖	mathematical	—	dblX WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_sub map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_dblXYZ 📖	mathematical	—	dblXYZ WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_dblX map_dblY map_dblZ comp_fin3
map_dblY 📖	mathematical	—	dblY WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_dblX map_negDblY map_dblZ map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_neg map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
map_dblZ 📖	mathematical	—	dblZ WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_sub RingHomClass.toAddMonoidHomClass map_neg
map_negAddY 📖	mathematical	—	negAddY WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_neg map_ofNat map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_negDblY 📖	mathematical	—	negDblY WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
map_negY 📖	mathematical	—	negY WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_neg map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
negAddY_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	negAddY DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WeierstrassCurve.a₁ WeierstrassCurve.a₂	—	negAddY_eq' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain mul_ne_zero
negAddY_eq' 📖	mathematical	Equation	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negAddY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing WeierstrassCurve.a₁ WeierstrassCurve.a₂	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange negAddY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.pow_bit1
negAddY_of_X_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negAddY NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing addU	—	addU.eq_1 neg_div neg_neg mul_div_mul_right mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain negAddY_of_X_eq' sq mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors
negAddY_of_X_eq' 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negAddY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	negAddY_eq' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_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.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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_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_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.pow_bit1
negAddY_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negAddY Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring negY	—	negAddY.eq_1 X_eq_zero_of_Z_eq_zero negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
negAddY_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negAddY Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring negY	—	negAddY.eq_1 X_eq_zero_of_Z_eq_zero negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add
negAddY_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing negAddY addZ WeierstrassCurve.Affine.negAddY toAffine WeierstrassCurve.Affine.slope	—	negAddY_eq addZ_eq sub_ne_zero
negAddY_self 📖	mathematical	—	negAddY MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	negAddY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.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_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.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
negAddY_smul 📖	mathematical	—	negAddY Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.neg_zero 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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
negDblY_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	negDblY DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring WeierstrassCurve.a₁ negY WeierstrassCurve.a₂ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat negDblY_eq' mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
negDblY_eq' 📖	mathematical	Equation	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negDblY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne WeierstrassCurve.a₁ negY WeierstrassCurve.a₂ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange negDblY.eq_1 eval_polynomialX negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_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.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 Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.pow_bit1
negDblY_of_Y_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	negDblY NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing dblU	—	dblU.eq_1 neg_div negDblY_of_Y_eq' IsDomain.to_noZeroDivisors instIsDomain mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass pow_ne_zero isReduced_of_noZeroDivisors
negDblY_of_Y_eq' 📖	mathematical	Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	negDblY Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval polynomialX	—	Nat.instAtLeastTwoHAddOfNat negDblY_eq' Y_eq_negY_of_Y_eq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.sub_congr 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.sub_pf 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.zero_pow Mathlib.Tactic.Ring.const_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
negDblY_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negDblY NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	negDblY.eq_1 X_eq_zero_of_Z_eq_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_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.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_congr Mathlib.Meta.NormNum.instAtLeastTwo 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.sub_pf Mathlib.Tactic.Ring.zero_pow Mathlib.Tactic.Ring.const_pos
negDblY_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing negDblY dblZ WeierstrassCurve.Affine.negAddY toAffine WeierstrassCurve.Affine.slope	—	Nat.instAtLeastTwoHAddOfNat negDblY_eq dblZ.eq_1 X_eq_iff sub_ne_zero Y_ne_negY_of_Y_ne' IsDomain.to_noZeroDivisors instIsDomain
negDblY_smul 📖	mathematical	—	negDblY Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_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.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.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 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.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
negY_eq 📖	mathematical	—	negY Matrix.vecCons Matrix.vecEmpty SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WeierstrassCurve.a₁ WeierstrassCurve.a₃	—	—
negY_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negY NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	negY.eq_1 X_eq_zero_of_Z_eq_zero MulZeroClass.mul_zero sub_zero
negY_of_Z_ne_zero 📖	mathematical	—	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing negY EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY toAffine	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq div_self Mathlib.Tactic.LinearCombination.eq_rearrange negY.eq_1 WeierstrassCurve.Affine.negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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_congr 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.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt 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 Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt 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 Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
negY_smul 📖	mathematical	—	negY Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_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.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
nonsingular_iff_of_Y_eq_negY 📖	mathematical	negY EuclideanDomain.toCommRing Field.toEuclideanDomain	Nonsingular Equation	—	negY.eq_1 Nat.instAtLeastTwoHAddOfNat eval_polynomialY Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr 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.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pp_pf_overlap nonsingular_iff_of_Z_ne_zero sub_self MulZeroClass.zero_mul

---

← Back to Index