CubicDiscriminant

📁 Source: Mathlib/Algebra/CubicDiscriminant.lean

Statistics

Metric	Count
Definitions Cubic, a, b, c, d, disc, discr, equiv, instInhabited, instZero, map, roots, toPoly	13
Theorems C_mul_prod_X_sub_C_eq, a_of_eq, b_eq_three_roots, b_of_eq, c_eq_three_roots, c_of_eq, card_roots_le, card_roots_of_disc_ne_zero, card_roots_of_discr_ne_zero, coeff_eq_a, coeff_eq_b, coeff_eq_c, coeff_eq_d, coeff_eq_zero, d_eq_three_roots, d_of_eq, degree_of_a_eq_zero, degree_of_a_eq_zero', degree_of_a_ne_zero, degree_of_a_ne_zero', degree_of_b_eq_zero, degree_of_b_eq_zero', degree_of_b_ne_zero, degree_of_b_ne_zero', degree_of_c_eq_zero, degree_of_c_eq_zero', degree_of_c_ne_zero, degree_of_c_ne_zero', degree_of_d_eq_zero, degree_of_d_eq_zero', degree_of_d_ne_zero, degree_of_d_ne_zero', degree_of_zero, disc_eq_prod_three_roots, disc_ne_zero_iff_roots_ne, disc_ne_zero_iff_roots_nodup, discr_eq_prod_three_roots, discr_ne_zero_iff_roots_ne, discr_ne_zero_iff_roots_nodup, eq_prod_three_roots, eq_sum_three_roots, equiv_apply_coe, equiv_symm_apply_a, equiv_symm_apply_b, equiv_symm_apply_c, equiv_symm_apply_d, ext, ext_iff, leadingCoeff_of_a_ne_zero, leadingCoeff_of_a_ne_zero', leadingCoeff_of_b_ne_zero, leadingCoeff_of_b_ne_zero', leadingCoeff_of_c_eq_zero, leadingCoeff_of_c_eq_zero', leadingCoeff_of_c_ne_zero, leadingCoeff_of_c_ne_zero', map_roots, map_toPoly, mem_roots_iff, monic_of_a_eq_one, monic_of_a_eq_one', monic_of_b_eq_one, monic_of_b_eq_one', monic_of_c_eq_one, monic_of_c_eq_one', monic_of_d_eq_one, monic_of_d_eq_one', natDegree_of_a_eq_zero, natDegree_of_a_eq_zero', natDegree_of_a_ne_zero, natDegree_of_a_ne_zero', natDegree_of_b_eq_zero, natDegree_of_b_eq_zero', natDegree_of_b_ne_zero, natDegree_of_b_ne_zero', natDegree_of_c_eq_zero, natDegree_of_c_eq_zero', natDegree_of_c_ne_zero, natDegree_of_c_ne_zero', natDegree_of_zero, ne_zero_of_a_ne_zero, ne_zero_of_b_ne_zero, ne_zero_of_c_ne_zero, ne_zero_of_d_ne_zero, of_a_eq_zero, of_a_eq_zero', of_b_eq_zero, of_b_eq_zero', of_c_eq_zero, of_c_eq_zero', of_d_eq_zero, of_d_eq_zero', prod_X_sub_C_eq, splits_iff_card_roots, splits_iff_roots_eq_three, toPoly_eq_zero_iff, toPoly_injective, zero	98
Total	111

Cubic

Definitions

Name	Category	Theorems
a 📖	CompOp	13 math math: ext_iff, disc_eq_prod_three_roots, c_eq_three_roots, mem_roots_iff, discr_eq_prod_three_roots, a_of_eq, leadingCoeff_of_a_ne_zero, eq_sum_three_roots, eq_prod_three_roots, equiv_symm_apply_a, d_eq_three_roots, b_eq_three_roots, coeff_eq_a
b 📖	CompOp	8 math math: ext_iff, coeff_eq_b, mem_roots_iff, of_a_eq_zero, equiv_symm_apply_b, b_of_eq, leadingCoeff_of_b_ne_zero, b_eq_three_roots
c 📖	CompOp	9 math math: ext_iff, c_eq_three_roots, coeff_eq_c, mem_roots_iff, of_a_eq_zero, of_b_eq_zero, equiv_symm_apply_c, c_of_eq, leadingCoeff_of_c_ne_zero
d 📖	CompOp	10 math math: d_of_eq, ext_iff, mem_roots_iff, of_a_eq_zero, of_b_eq_zero, coeff_eq_d, leadingCoeff_of_c_eq_zero, equiv_symm_apply_d, d_eq_three_roots, of_c_eq_zero
disc 📖	CompOp	—
discr 📖	CompOp	10 math math: WeierstrassCurve.twoTorsionPolynomial_discr_of_char_three, WeierstrassCurve.twoTorsionPolynomial_disc_of_char_three, disc_eq_prod_three_roots, discr_eq_prod_three_roots, WeierstrassCurve.twoTorsionPolynomial_disc_of_char_two, WeierstrassCurve.twoTorsionPolynomial_discr_isUnit, WeierstrassCurve.twoTorsionPolynomial_disc_isUnit, WeierstrassCurve.twoTorsionPolynomial_disc, WeierstrassCurve.twoTorsionPolynomial_discr_of_char_two, WeierstrassCurve.twoTorsionPolynomial_discr
equiv 📖	CompOp	5 math math: equiv_symm_apply_b, equiv_symm_apply_c, equiv_apply_coe, equiv_symm_apply_d, equiv_symm_apply_a
instInhabited 📖	CompOp	—
instZero 📖	CompOp	4 math math: zero, natDegree_of_zero, toPoly_eq_zero_iff, degree_of_zero
map 📖	CompOp	8 math math: splits_iff_card_roots, card_roots_of_disc_ne_zero, card_roots_of_discr_ne_zero, disc_ne_zero_iff_roots_nodup, splits_iff_roots_eq_three, discr_ne_zero_iff_roots_nodup, map_roots, map_toPoly
roots 📖	CompOp	9 math math: mem_roots_iff, splits_iff_card_roots, card_roots_of_disc_ne_zero, card_roots_of_discr_ne_zero, disc_ne_zero_iff_roots_nodup, splits_iff_roots_eq_three, card_roots_le, discr_ne_zero_iff_roots_nodup, map_roots
toPoly 📖	CompOp	73 math math: of_a_eq_zero', degree_of_b_eq_zero, natDegree_of_b_ne_zero, coeff_eq_b, natDegree_of_c_ne_zero, coeff_eq_c, monic_of_c_eq_one, WeierstrassCurve.Affine.polynomial_eq, splits_iff_card_roots, degree_of_a_eq_zero', coeff_eq_zero, degree_of_a_ne_zero', of_a_eq_zero, of_b_eq_zero, coeff_eq_d, of_d_eq_zero, leadingCoeff_of_b_ne_zero', degree_of_d_ne_zero, natDegree_of_a_ne_zero, of_c_eq_zero', natDegree_of_b_eq_zero', of_b_eq_zero', WeierstrassCurve.Ψ₂Sq_eq, degree_of_d_eq_zero, toPoly_injective, WeierstrassCurve.Affine.addPolynomial_eq, splits_iff_roots_eq_three, natDegree_of_c_eq_zero, leadingCoeff_of_c_eq_zero', leadingCoeff_of_a_ne_zero, natDegree_of_a_eq_zero', monic_of_a_eq_one', natDegree_of_c_eq_zero', monic_of_b_eq_one', monic_of_c_eq_one', degree_of_a_eq_zero, natDegree_of_a_eq_zero, prod_X_sub_C_eq, degree_of_c_ne_zero, degree_of_a_ne_zero, monic_of_a_eq_one, zero, degree_of_d_eq_zero', natDegree_of_zero, equiv_apply_coe, of_d_eq_zero', leadingCoeff_of_c_eq_zero, degree_of_b_ne_zero', degree_of_b_eq_zero', natDegree_of_b_ne_zero', degree_of_c_ne_zero', degree_of_d_ne_zero', monic_of_d_eq_one', eq_prod_three_roots, map_roots, leadingCoeff_of_c_ne_zero, toPoly_eq_zero_iff, monic_of_d_eq_one, degree_of_c_eq_zero, natDegree_of_c_ne_zero', leadingCoeff_of_b_ne_zero, map_toPoly, leadingCoeff_of_a_ne_zero', C_mul_prod_X_sub_C_eq, natDegree_of_a_ne_zero', degree_of_c_eq_zero', leadingCoeff_of_c_ne_zero', monic_of_b_eq_one, coeff_eq_a, of_c_eq_zero, degree_of_zero, degree_of_b_ne_zero, natDegree_of_b_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_mul_prod_X_sub_C_eq 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.instSub CommRing.toRing Polynomial.X toPoly Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toAdd	—	Polynomial.C_mul Polynomial.C_neg Polynomial.C_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_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_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_congr
a_of_eq 📖	mathematical	toPoly	a	—	coeff_eq_a
b_eq_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike b Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Distrib.toAdd	—	instIsDomain eq_sum_three_roots
b_of_eq 📖	mathematical	toPoly	b	—	coeff_eq_b
c_eq_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike c Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a Distrib.toAdd	—	instIsDomain eq_sum_three_roots
c_of_eq 📖	mathematical	toPoly	c	—	coeff_eq_c
card_roots_le 📖	mathematical	—	Finset.card Multiset.toFinset roots	—	LE.le.trans Multiset.toFinset_card_le Polynomial.card_roots' Polynomial.natDegree_zero zero_le Nat.instCanonicallyOrderedAdd WithBot.coe_le_coe Polynomial.card_roots Polynomial.degree_cubic_le
card_roots_of_disc_ne_zero 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly	Finset.card Multiset.toFinset roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map	—	card_roots_of_discr_ne_zero
card_roots_of_discr_ne_zero 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly	Finset.card Multiset.toFinset roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map	—	instIsDomain Multiset.toFinset_card_of_nodup discr_ne_zero_iff_roots_nodup splits_iff_card_roots
coeff_eq_a 📖	mathematical	—	Polynomial.coeff toPoly a	—	—
coeff_eq_b 📖	mathematical	—	Polynomial.coeff toPoly b	—	—
coeff_eq_c 📖	mathematical	—	Polynomial.coeff toPoly c	—	—
coeff_eq_d 📖	mathematical	—	Polynomial.coeff toPoly d	—	—
coeff_eq_zero 📖	mathematical	—	Polynomial.coeff toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
d_eq_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike d Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	instIsDomain eq_sum_three_roots
d_of_eq 📖	mathematical	toPoly	d	—	coeff_eq_d
degree_of_a_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat of_a_eq_zero Polynomial.degree_quadratic_le
degree_of_a_eq_zero' 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	degree_of_a_eq_zero
degree_of_a_ne_zero 📖	mathematical	—	Polynomial.degree toPoly WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Polynomial.degree_cubic
degree_of_a_ne_zero' 📖	mathematical	—	Polynomial.degree toPoly WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat degree_of_a_ne_zero
degree_of_b_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly WithBot.one Nat.instOne	—	of_b_eq_zero Polynomial.degree_linear_le
degree_of_b_eq_zero' 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot.one Nat.instOne	—	degree_of_b_eq_zero
degree_of_b_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Polynomial.degree toPoly WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat of_a_eq_zero Polynomial.degree_quadratic
degree_of_b_ne_zero' 📖	mathematical	—	Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat degree_of_b_ne_zero
degree_of_c_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly WithBot.zero Nat.instMulZeroClass	—	of_c_eq_zero Polynomial.degree_C_le
degree_of_c_eq_zero' 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot.zero Nat.instMulZeroClass	—	degree_of_c_eq_zero
degree_of_c_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	Polynomial.degree toPoly WithBot WithBot.one Nat.instOne	—	of_b_eq_zero Polynomial.degree_linear
degree_of_c_ne_zero' 📖	mathematical	—	Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot WithBot.one Nat.instOne	—	degree_of_c_ne_zero
degree_of_d_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c d	Polynomial.degree toPoly Bot.bot WithBot WithBot.bot	—	of_d_eq_zero Polynomial.degree_zero
degree_of_d_eq_zero' 📖	mathematical	—	Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Bot.bot WithBot WithBot.bot	—	degree_of_d_eq_zero
degree_of_d_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c	Polynomial.degree toPoly WithBot WithBot.zero Nat.instMulZeroClass	—	of_c_eq_zero Polynomial.degree_C
degree_of_d_ne_zero' 📖	mathematical	—	Polynomial.degree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot WithBot.zero Nat.instMulZeroClass	—	degree_of_d_ne_zero
degree_of_zero 📖	mathematical	—	Polynomial.degree toPoly Cubic instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Bot.bot WithBot WithBot.bot	—	degree_of_d_eq_zero'
disc_eq_prod_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike discr DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	discr_eq_prod_three_roots
disc_ne_zero_iff_roots_ne 📖	—	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	—	—	discr_ne_zero_iff_roots_ne
disc_ne_zero_iff_roots_nodup 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly	Multiset.Nodup roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map	—	discr_ne_zero_iff_roots_nodup
discr_eq_prod_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike discr DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing a SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	instIsDomain RingHom.map_add map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_ofNat b_eq_three_roots c_eq_three_roots d_eq_three_roots Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.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.isNat_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_bit1 Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.intPow_negOfNat_bit0 Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
discr_ne_zero_iff_roots_ne 📖	—	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	—	—	instIsDomain map_ne_zero EuclideanDomain.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass discr_eq_prod_three_roots pow_two IsDomain.to_noZeroDivisors
discr_ne_zero_iff_roots_nodup 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly	Multiset.Nodup roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map	—	instIsDomain splits_iff_roots_eq_three discr_ne_zero_iff_roots_ne Multiset.nodup_cons Multiset.mem_cons Multiset.mem_singleton
eq_prod_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	toPoly Polynomial Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C a Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X	—	instIsDomain map_toPoly Polynomial.Splits.eq_prod_roots splits_iff_roots_eq_three Polynomial.leadingCoeff_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial leadingCoeff_of_a_ne_zero map_roots Multiset.prod_cons Multiset.prod_singleton mul_assoc
eq_sum_three_roots 📖	mathematical	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Multiset Multiset.instInsert Multiset.instSingleton	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike a Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Distrib.toAdd	—	instIsDomain toPoly_injective eq_prod_three_roots C_mul_prod_X_sub_C_eq
equiv_apply_coe 📖	mathematical	—	Polynomial WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne DFunLike.coe Equiv Cubic Nat.instAtLeastTwoHAddOfNat EquivLike.toFunLike Equiv.instEquivLike equiv toPoly	—	Nat.instAtLeastTwoHAddOfNat
equiv_symm_apply_a 📖	mathematical	—	a DFunLike.coe Equiv Polynomial WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Cubic EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv Polynomial.coeff	—	Nat.instAtLeastTwoHAddOfNat
equiv_symm_apply_b 📖	mathematical	—	b DFunLike.coe Equiv Polynomial WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Cubic EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv Polynomial.coeff	—	Nat.instAtLeastTwoHAddOfNat
equiv_symm_apply_c 📖	mathematical	—	c DFunLike.coe Equiv Polynomial WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Cubic EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv Polynomial.coeff	—	Nat.instAtLeastTwoHAddOfNat
equiv_symm_apply_d 📖	mathematical	—	d DFunLike.coe Equiv Polynomial WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Cubic EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv Polynomial.coeff	—	Nat.instAtLeastTwoHAddOfNat
ext 📖	—	a b c d	—	—	—
ext_iff 📖	mathematical	—	a b c d	—	ext
leadingCoeff_of_a_ne_zero 📖	mathematical	—	Polynomial.leadingCoeff toPoly a	—	Polynomial.leadingCoeff_cubic
leadingCoeff_of_a_ne_zero' 📖	mathematical	—	Polynomial.leadingCoeff toPoly	—	leadingCoeff_of_a_ne_zero
leadingCoeff_of_b_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Polynomial.leadingCoeff toPoly b	—	of_a_eq_zero Polynomial.leadingCoeff_quadratic
leadingCoeff_of_b_ne_zero' 📖	mathematical	—	Polynomial.leadingCoeff toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	leadingCoeff_of_b_ne_zero
leadingCoeff_of_c_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c	Polynomial.leadingCoeff toPoly d	—	of_c_eq_zero Polynomial.leadingCoeff_C
leadingCoeff_of_c_eq_zero' 📖	mathematical	—	Polynomial.leadingCoeff toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	leadingCoeff_of_c_eq_zero
leadingCoeff_of_c_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	Polynomial.leadingCoeff toPoly c	—	of_b_eq_zero Polynomial.leadingCoeff_linear
leadingCoeff_of_c_ne_zero' 📖	mathematical	—	Polynomial.leadingCoeff toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	leadingCoeff_of_c_ne_zero
map_roots 📖	mathematical	—	roots map CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.roots Polynomial.map toPoly	—	roots.eq_1 map_toPoly
map_toPoly 📖	mathematical	—	toPoly map Polynomial.map	—	Polynomial.map_add Polynomial.map_mul Polynomial.map_C Polynomial.map_pow Polynomial.map_X
mem_roots_iff 📖	mathematical	—	Multiset Multiset.instMembership roots Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul a Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring b c d MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	roots.eq_1 Polynomial.mem_roots Polynomial.IsRoot.eq_1 toPoly.eq_1 Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_pow Polynomial.eval_X
monic_of_a_eq_one 📖	mathematical	a AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Polynomial.Monic toPoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.Monic.eq_1 leadingCoeff_of_a_ne_zero one_ne_zero NeZero.one
monic_of_a_eq_one' 📖	mathematical	—	Polynomial.Monic toPoly AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	monic_of_a_eq_one
monic_of_b_eq_one 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Polynomial.Monic toPoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.Monic.eq_1 leadingCoeff_of_b_ne_zero one_ne_zero NeZero.one
monic_of_b_eq_one' 📖	mathematical	—	Polynomial.Monic toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monic_of_b_eq_one
monic_of_c_eq_one 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Polynomial.Monic toPoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.Monic.eq_1 leadingCoeff_of_c_ne_zero one_ne_zero NeZero.one
monic_of_c_eq_one' 📖	mathematical	—	Polynomial.Monic toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monic_of_c_eq_one
monic_of_d_eq_one 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c d AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Polynomial.Monic toPoly	—	Polynomial.Monic.eq_1 leadingCoeff_of_c_eq_zero
monic_of_d_eq_one' 📖	mathematical	—	Polynomial.Monic Nat.instSemiring toPoly	—	monic_of_d_eq_one
natDegree_of_a_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Polynomial.natDegree toPoly	—	of_a_eq_zero Polynomial.natDegree_quadratic_le
natDegree_of_a_eq_zero' 📖	mathematical	—	Polynomial.natDegree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_a_eq_zero
natDegree_of_a_ne_zero 📖	mathematical	—	Polynomial.natDegree toPoly	—	Polynomial.natDegree_cubic
natDegree_of_a_ne_zero' 📖	mathematical	—	Polynomial.natDegree toPoly	—	natDegree_of_a_ne_zero
natDegree_of_b_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	Polynomial.natDegree toPoly	—	of_b_eq_zero Polynomial.natDegree_linear_le
natDegree_of_b_eq_zero' 📖	mathematical	—	Polynomial.natDegree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_b_eq_zero
natDegree_of_b_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Polynomial.natDegree toPoly	—	of_a_eq_zero Polynomial.natDegree_quadratic
natDegree_of_b_ne_zero' 📖	mathematical	—	Polynomial.natDegree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_b_ne_zero
natDegree_of_c_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c	Polynomial.natDegree toPoly	—	of_c_eq_zero Polynomial.natDegree_C
natDegree_of_c_eq_zero' 📖	mathematical	—	Polynomial.natDegree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_c_eq_zero
natDegree_of_c_ne_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	Polynomial.natDegree toPoly	—	of_b_eq_zero Polynomial.natDegree_linear
natDegree_of_c_ne_zero' 📖	mathematical	—	Polynomial.natDegree toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_c_ne_zero
natDegree_of_zero 📖	mathematical	—	Polynomial.natDegree toPoly Cubic instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	natDegree_of_c_eq_zero'
ne_zero_of_a_ne_zero 📖	—	—	—	—	—
ne_zero_of_b_ne_zero 📖	—	—	—	—	—
ne_zero_of_c_ne_zero 📖	—	—	—	—	—
ne_zero_of_d_ne_zero 📖	—	—	—	—	—
of_a_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	toPoly Polynomial Polynomial.instAdd Polynomial.instMul DFunLike.coe RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C b Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X c d	—	toPoly.eq_1 Polynomial.C_0 MulZeroClass.zero_mul zero_add
of_a_eq_zero' 📖	mathematical	—	toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial Polynomial.instAdd Polynomial.instMul DFunLike.coe RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	of_a_eq_zero
of_b_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b	toPoly Polynomial Polynomial.instAdd Polynomial.instMul DFunLike.coe RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C c Polynomial.X d	—	of_a_eq_zero Polynomial.C_0 MulZeroClass.zero_mul zero_add
of_b_eq_zero' 📖	mathematical	—	toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial Polynomial.instAdd Polynomial.instMul DFunLike.coe RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.X	—	of_b_eq_zero
of_c_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c	toPoly DFunLike.coe RingHom Polynomial Polynomial.semiring RingHom.instFunLike Polynomial.C d	—	of_b_eq_zero Polynomial.C_0 MulZeroClass.zero_mul zero_add
of_c_eq_zero' 📖	mathematical	—	toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom Polynomial Polynomial.semiring RingHom.instFunLike Polynomial.C	—	of_c_eq_zero
of_d_eq_zero 📖	mathematical	a MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring b c d	toPoly Polynomial Polynomial.instZero	—	of_c_eq_zero Polynomial.C_0
of_d_eq_zero' 📖	mathematical	—	toPoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial Polynomial.instZero	—	of_d_eq_zero
prod_X_sub_C_eq 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C toPoly AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul	—	one_mul Polynomial.C_1 C_mul_prod_X_sub_C_eq
splits_iff_card_roots 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly Multiset.card roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map	—	map_ne_zero EuclideanDomain.toNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsDomain roots.eq_1 map_toPoly Polynomial.splits_iff_card_roots Polynomial.degree_eq_iff_natDegree_eq ne_zero_of_a_ne_zero degree_of_a_ne_zero
splits_iff_roots_eq_three 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map toPoly roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain map Multiset Multiset.instInsert Multiset.instSingleton	—	instIsDomain splits_iff_card_roots Multiset.card_eq_three
toPoly_eq_zero_iff 📖	mathematical	—	toPoly Polynomial Polynomial.instZero Cubic instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	zero toPoly_injective
toPoly_injective 📖	mathematical	—	toPoly	—	ext a_of_eq b_of_eq c_of_eq d_of_eq
zero 📖	mathematical	—	toPoly Cubic instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial Polynomial.instZero	—	of_d_eq_zero'

(root)

Definitions

Name	Category	Theorems
Cubic 📖	CompData	9 math math: Cubic.equiv_symm_apply_b, Cubic.equiv_symm_apply_c, Cubic.zero, Cubic.natDegree_of_zero, Cubic.equiv_apply_coe, Cubic.equiv_symm_apply_d, Cubic.toPoly_eq_zero_iff, Cubic.equiv_symm_apply_a, Cubic.degree_of_zero

---

← Back to Index