Formula

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

Statistics

Metric	Count
Definitions addPolynomial, addX, addY, linePolynomial, negAddY, negPolynomial, negY, slope	8
Theorems C_addPolynomial, C_addPolynomial_slope, Y_eq_of_X_eq, Y_eq_of_Y_ne, Y_sub_negPolynomial, Y_sub_polynomialY, addPolynomial_eq, addPolynomial_slope, addX_eq_addX_negY_sub, addY_sub_negY_addY, baseChange_addPolynomial, baseChange_addX, baseChange_addY, baseChange_negAddY, baseChange_negPolynomial, baseChange_negY, baseChange_slope, cyclic_sum_Y_mul_X_sub_X, derivative_addPolynomial_slope, equation_add, equation_add_iff, equation_neg, equation_negAdd, evalEval_negPolynomial, map_addPolynomial, map_addX, map_addY, map_linePolynomial, map_negAddY, map_negPolynomial, map_negY, map_slope, negY_negY, nonsingular_add, nonsingular_neg, nonsingular_negAdd, nonsingular_negAdd_of_eval_derivative_ne_zero, slope_of_X_ne, slope_of_Y_eq, slope_of_Y_ne, slope_of_Y_ne', slope_of_Y_ne_eq_evalEval	42
Total	50

WeierstrassCurve.Affine

Definitions

Name	Category	Theorems
addPolynomial 📖	CompOp	10 math math: C_addPolynomial, CoordinateRing.C_addPolynomial, addPolynomial_slope, C_addPolynomial_slope, derivative_addPolynomial_slope, addPolynomial_eq, baseChange_addPolynomial, CoordinateRing.C_addPolynomial_slope, equation_add_iff, map_addPolynomial
addX 📖	CompOp	38 math math: WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero, nonsingular_negAdd, WeierstrassCurve.Jacobian.add_of_Y_ne', cyclic_sum_Y_mul_X_sub_X, WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero, Point.add_self_of_Y_ne, Point.add_of_X_ne, CoordinateRing.XYIdeal_add_eq, addPolynomial_slope, WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Jacobian.addX_of_Z_ne_zero, addX_eq_addX_negY_sub, C_addPolynomial_slope, Point.add_self_of_Y_ne', derivative_addPolynomial_slope, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, addY_sub_negY_addY, Point.add_of_Y_ne, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, CoordinateRing.C_addPolynomial_slope, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', equation_add_iff, nonsingular_add, WeierstrassCurve.Jacobian.add_of_X_ne, Point.add_some, WeierstrassCurve.Projective.add_of_X_ne, WeierstrassCurve.Projective.add_of_Y_ne', WeierstrassCurve.Projective.addMap_of_Z_ne_zero, Point.add_of_Y_ne', Point.add_of_X_ne', equation_negAdd, WeierstrassCurve.Projective.addX_of_Z_ne_zero, baseChange_addX, WeierstrassCurve.Projective.dblX_of_Z_ne_zero, map_addX, CoordinateRing.XYIdeal_mul_XYIdeal, equation_add
addY 📖	CompOp	26 math math: WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero, WeierstrassCurve.Jacobian.add_of_Y_ne', Point.add_self_of_Y_ne, map_addY, WeierstrassCurve.Projective.addY_of_Z_ne_zero, Point.add_of_X_ne, CoordinateRing.XYIdeal_add_eq, WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Jacobian.addY_of_Z_ne_zero, WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, addY_sub_negY_addY, Point.add_of_Y_ne, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', nonsingular_add, WeierstrassCurve.Jacobian.add_of_X_ne, WeierstrassCurve.Projective.dblY_of_Z_ne_zero, Point.add_some, WeierstrassCurve.Projective.add_of_X_ne, WeierstrassCurve.Projective.add_of_Y_ne', WeierstrassCurve.Projective.addMap_of_Z_ne_zero, baseChange_addY, CoordinateRing.XYIdeal_mul_XYIdeal, equation_add
linePolynomial 📖	CompOp	7 math math: CoordinateRing.XYIdeal_eq₂, C_addPolynomial, map_linePolynomial, CoordinateRing.C_addPolynomial, CoordinateRing.XYIdeal_add_eq, CoordinateRing.XYIdeal_eq₁, CoordinateRing.XYIdeal_mul_XYIdeal
negAddY 📖	CompOp	13 math math: nonsingular_negAdd, cyclic_sum_Y_mul_X_sub_X, Point.add_self_of_Y_ne', WeierstrassCurve.Projective.negDblY_of_Z_ne_zero, equation_add_iff, map_negAddY, WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero, Point.add_of_Y_ne', Point.add_of_X_ne', WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero, equation_negAdd, WeierstrassCurve.Projective.negAddY_of_Z_ne_zero, baseChange_negAddY
negPolynomial 📖	CompOp	8 math math: Y_sub_negPolynomial, C_addPolynomial, baseChange_negPolynomial, CoordinateRing.C_addPolynomial, CoordinateRing.XYIdeal_add_eq, map_negPolynomial, Y_sub_polynomialY, evalEval_negPolynomial
negY 📖	CompOp	27 math math: Point.add_self_of_Y_ne, WeierstrassCurve.Projective.Y_eq_iff', WeierstrassCurve.Jacobian.negY_of_Z_ne_zero, baseChange_negY, Point.add_of_X_ne, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, slope_of_Y_ne, CoordinateRing.mk_XYIdeal'_neg_mul, WeierstrassCurve.Projective.negY_of_Z_ne_zero, addX_eq_addX_negY_sub, Point.add_self_of_Y_ne', Y_eq_of_X_eq, Point.neg_some, addY_sub_negY_addY, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, equation_neg, Point.add_of_Y_ne, WeierstrassCurve.Projective.neg_of_Z_ne_zero, CoordinateRing.XYIdeal_neg_mul, WeierstrassCurve.Jacobian.Y_eq_iff', Point.add_of_Y_ne', Point.add_of_X_ne', WeierstrassCurve.Jacobian.neg_of_Z_ne_zero, map_negY, negY_negY, evalEval_negPolynomial, nonsingular_neg
slope 📖	CompOp	50 math math: WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero, nonsingular_negAdd, WeierstrassCurve.Jacobian.add_of_Y_ne', cyclic_sum_Y_mul_X_sub_X, WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero, Point.add_self_of_Y_ne, CoordinateRing.XYIdeal_eq₂, WeierstrassCurve.Projective.addY_of_Z_ne_zero, Point.add_of_X_ne, slope_of_Y_ne, slope_of_Y_ne', addPolynomial_slope, WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Jacobian.addX_of_Z_ne_zero, addX_eq_addX_negY_sub, slope_of_X_ne, C_addPolynomial_slope, Point.add_self_of_Y_ne', WeierstrassCurve.Jacobian.addY_of_Z_ne_zero, WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero, derivative_addPolynomial_slope, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, map_slope, WeierstrassCurve.Projective.negDblY_of_Z_ne_zero, addY_sub_negY_addY, Point.add_of_Y_ne, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, CoordinateRing.C_addPolynomial_slope, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', nonsingular_add, WeierstrassCurve.Jacobian.add_of_X_ne, WeierstrassCurve.Projective.dblY_of_Z_ne_zero, Point.add_some, slope_of_Y_ne_eq_evalEval, slope_of_Y_eq, WeierstrassCurve.Projective.add_of_X_ne, WeierstrassCurve.Projective.add_of_Y_ne', WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, baseChange_slope, Point.add_of_Y_ne', Point.add_of_X_ne', WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero, equation_negAdd, WeierstrassCurve.Projective.addX_of_Z_ne_zero, WeierstrassCurve.Projective.negAddY_of_Z_ne_zero, WeierstrassCurve.Projective.dblX_of_Z_ne_zero, CoordinateRing.XYIdeal_mul_XYIdeal, equation_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_addPolynomial 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C addPolynomial Polynomial.instAdd Polynomial.instMul Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.X linePolynomial negPolynomial polynomial	—	addPolynomial.eq_1 linePolynomial.eq_1 polynomial.eq_1 negPolynomial.eq_1 Polynomial.eval_sub Polynomial.eval_add Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_mul Polynomial.eval_C Polynomial.C_sub Polynomial.C_add Polynomial.C_pow Polynomial.C_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.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_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.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.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
C_addPolynomial_slope 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain negY	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C addPolynomial slope Polynomial.instNeg Polynomial.ring DivisionRing.toRing Field.toDivisionRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul Polynomial.instSub Polynomial.X addX	—	addPolynomial_slope map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_neg
Y_eq_of_X_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	negY	—	sub_eq_zero mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain negY.eq_1 Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq equation_iff 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.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_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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt 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 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
Y_eq_of_Y_ne 📖	—	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—	Y_eq_of_X_eq
Y_sub_negPolynomial 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.X negPolynomial polynomialY	—	Y_sub_polynomialY sub_sub_cancel
Y_sub_polynomialY 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.X polynomialY negPolynomial	—	polynomialY.eq_1 negPolynomial.eq_1 map_ofNat RingHom.instRingHomClass Polynomial.C_add Polynomial.C_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_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 Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr
addPolynomial_eq 📖	mathematical	—	addPolynomial Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instNeg CommRing.toRing Cubic.toPoly AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul WeierstrassCurve.a₁ WeierstrassCurve.a₂ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.a₃ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	Nat.instAtLeastTwoHAddOfNat addPolynomial.eq_1 linePolynomial.eq_1 polynomial.eq_1 Cubic.toPoly.eq_1 Polynomial.eval_sub Polynomial.eval_add Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_mul Polynomial.eval_C Polynomial.C_add Polynomial.C_sub Polynomial.C_neg Polynomial.C_pow Polynomial.C_mul map_ofNat RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.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_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.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.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo
addPolynomial_slope 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain negY	addPolynomial slope Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instNeg DivisionRing.toRing Field.toDivisionRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C addX	—	Nat.instAtLeastTwoHAddOfNat addPolynomial_eq Cubic.prod_X_sub_C_eq Cubic.toPoly_injective slope_of_Y_ne Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_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.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 sub_ne_zero negY.eq_1 Cubic.ext Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.div_pf Mathlib.Tactic.Ring.atom_pf' 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_mul Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero neg_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add 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.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ 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.eval_cons_mul_eval mul_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial add_sub_cancel Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange MulZeroClass.mul_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Y_eq_of_Y_ne slope_of_X_ne
addX_eq_addX_negY_sub 📖	mathematical	—	addX EuclideanDomain.toCommRing Field.toEuclideanDomain slope SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing negY DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	slope_of_X_ne neg_sub neg_sq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.zpow'_ofNat mul_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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_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.mul_one Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt 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_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.pow_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isNat_mul
addY_sub_negY_addY 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing addY EuclideanDomain.toCommRing Field.toEuclideanDomain slope negY addX DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eq_div_iff sub_ne_zero Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq cyclic_sum_Y_mul_X_sub_X 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.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.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.Meta.NormNum.IsNat.to_raw_eq 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.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_one 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_pf_add_gt Mathlib.Meta.NormNum.isNat_add
baseChange_addPolynomial 📖	mathematical	—	addPolynomial WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike Polynomial.map RingHomClass.toRingHom Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addPolynomial WeierstrassCurve.map_baseChange
baseChange_addX 📖	mathematical	—	addX WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addX WeierstrassCurve.map_baseChange
baseChange_addY 📖	mathematical	—	addY WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_addY WeierstrassCurve.map_baseChange
baseChange_negAddY 📖	mathematical	—	negAddY WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_negAddY WeierstrassCurve.map_baseChange
baseChange_negPolynomial 📖	mathematical	—	negPolynomial WeierstrassCurve.toAffine WeierstrassCurve.baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_negPolynomial WeierstrassCurve.map_baseChange
baseChange_negY 📖	mathematical	—	negY WeierstrassCurve.toAffine WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_negY WeierstrassCurve.map_baseChange
baseChange_slope 📖	mathematical	—	slope WeierstrassCurve.toAffine 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_slope WeierstrassCurve.map_baseChange
cyclic_sum_Y_mul_X_sub_X 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing addX slope negAddY MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	slope_of_X_ne Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg sub_ne_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial MulZeroClass.mul_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_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_gt Mathlib.Tactic.Ring.add_pf_add_zero 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.add_mul Mathlib.Tactic.Ring.mul_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.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul 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.pow_bit1 Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
derivative_addPolynomial_slope 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain negY	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative addPolynomial slope Polynomial.instNeg DivisionRing.toRing Field.toDivisionRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instAdd Polynomial.instMul Polynomial.instSub Polynomial.X RingHom RingHom.instFunLike Polynomial.C addX	—	addPolynomial_slope Polynomial.derivative_neg Polynomial.derivative_mul Polynomial.derivative_sub Polynomial.derivative_X Polynomial.derivative_C Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one 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.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
equation_add 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain negY	addX slope addY	—	equation_neg equation_negAdd
equation_add_iff 📖	mathematical	—	Equation addX negAddY Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring addPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Equation.eq_1 negAddY.eq_1 addPolynomial.eq_1 linePolynomial.eq_1 polynomial.eq_1 Polynomial.eval_sub Polynomial.eval_add Polynomial.eval_pow Polynomial.eval_X Polynomial.eval_mul Polynomial.eval_C
equation_neg 📖	mathematical	—	Equation negY	—	equation_iff negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_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.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.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow
equation_negAdd 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain negY	addX slope negAddY	—	equation_add_iff addPolynomial_slope Polynomial.eval_neg Polynomial.eval_mul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C neg_eq_zero sub_self MulZeroClass.mul_zero
evalEval_negPolynomial 📖	mathematical	—	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring negPolynomial negY	—	negY.eq_1 sub_sub negPolynomial.eq_1 Polynomial.eval_sub Polynomial.eval_neg Polynomial.eval_X Polynomial.eval_C Polynomial.eval_add Polynomial.eval_mul
map_addPolynomial 📖	mathematical	—	addPolynomial WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Polynomial.map	—	addPolynomial.eq_1 map_polynomial Polynomial.eval_map linePolynomial.eq_1 Polynomial.coe_mapRingHom Polynomial.eval₂_hom Polynomial.map_add Polynomial.map_mul Polynomial.map_C Polynomial.map_sub Polynomial.map_X
map_addX 📖	mathematical	—	addX WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
map_addY 📖	mathematical	—	addY WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_addX map_negAddY map_negY
map_linePolynomial 📖	mathematical	—	linePolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Polynomial.map	—	Polynomial.map_add Polynomial.map_mul Polynomial.map_C Polynomial.map_sub Polynomial.map_X
map_negAddY 📖	mathematical	—	negAddY WeierstrassCurve.toAffine WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_addX map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_sub
map_negPolynomial 📖	mathematical	—	negPolynomial WeierstrassCurve.toAffine WeierstrassCurve.map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Polynomial.map_sub Polynomial.map_neg Polynomial.map_X Polynomial.map_add Polynomial.map_mul Polynomial.map_C
map_negY 📖	mathematical	—	negY WeierstrassCurve.toAffine 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
map_slope 📖	mathematical	—	slope WeierstrassCurve.toAffine WeierstrassCurve.map EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	slope_of_Y_eq map_negY map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Nat.instAtLeastTwoHAddOfNat slope_of_Y_ne RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing map_div₀ map_sub RingHomClass.toAddMonoidHomClass map_add AddMonoidHomClass.toAddHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat map_pow MonoidWithZeroHomClass.toMonoidHomClass slope_of_X_ne
negY_negY 📖	mathematical	—	negY	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_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.Meta.NormNum.IsNat.to_raw_eq 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
nonsingular_add 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain negY	addX slope addY	—	nonsingular_neg nonsingular_negAdd
nonsingular_neg 📖	mathematical	—	Nonsingular negY	—	Nat.instAtLeastTwoHAddOfNat nonsingular_iff equation_neg negY.eq_1 negY_negY not_and_or
nonsingular_negAdd 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain negY	addX slope negAddY	—	negAddY.eq_1 sub_self MulZeroClass.mul_zero zero_add neg_sub mul_neg slope_of_X_ne div_mul_cancel₀ sub_ne_zero_of_ne sub_add_cancel nonsingular_negAdd_of_eval_derivative_ne_zero equation_negAdd derivative_addPolynomial_slope Polynomial.eval_neg Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C add_zero mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain
nonsingular_negAdd_of_eval_derivative_ne_zero 📖	mathematical	Equation addX negAddY	Nonsingular	—	Nonsingular.eq_1 negAddY.eq_1 polynomialX.eq_1 polynomialY.eq_1 Polynomial.eval_sub Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_X Polynomial.eval_add Polynomial.eval_pow Mathlib.Tactic.Contrapose.contrapose₂ addPolynomial.eq_1 linePolynomial.eq_1 polynomial.eq_1 Nat.instAtLeastTwoHAddOfNat Polynomial.derivative_sub Polynomial.derivative_add Polynomial.derivative_sq Polynomial.derivative_mul Polynomial.derivative_C Polynomial.derivative_X Polynomial.derivative_X_pow MulZeroClass.zero_mul sub_zero mul_one zero_add add_zero Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_natSub 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.Tactic.Ring.atom_pf 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_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.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_overlap Mathlib.Tactic.Ring.add_overlap_pf 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.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
slope_of_X_ne 📖	mathematical	—	slope DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	slope.eq_1
slope_of_Y_eq 📖	mathematical	negY EuclideanDomain.toCommRing Field.toEuclideanDomain	slope MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	slope.eq_1
slope_of_Y_ne 📖	mathematical	—	slope DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₁ negY	—	Nat.instAtLeastTwoHAddOfNat slope_of_Y_ne'
slope_of_Y_ne' 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.a₁ WeierstrassCurve.a₃	slope DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Distrib.toAdd instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WeierstrassCurve.a₂ WeierstrassCurve.a₄	—	Nat.instAtLeastTwoHAddOfNat
slope_of_Y_ne_eq_evalEval 📖	mathematical	—	slope DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain polynomialX polynomialY	—	Nat.instAtLeastTwoHAddOfNat slope_of_Y_ne evalEval_polynomialX neg_sub negY.eq_1 evalEval_polynomialY Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_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.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_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one

---

← Back to Index