Div

📁 Source: Mathlib/Algebra/Polynomial/Div.lean

Statistics

Metric	Count
Definitions decidableDvdMonic, divByMonic, divModByMonicAux, modByMonic, rootMultiplicity, «term_%ₘ_», «term_/ₘ_»	7
Theorems isRoot_eq_bot_of_natDegree_ne_one, not_isRoot_of_natDegree_ne_one, subsingleton_isRoot, dvd_coeff_zero, X_dvd_iff, X_dvd_sub_C, X_pow_dvd_iff, X_sub_C_dvd_sub_C_eval, add_modByMonic, associated_of_dvd_of_degree_eq, associated_of_dvd_of_natDegree_le, associated_of_dvd_of_natDegree_le_of_leadingCoeff, coeff_divByMonic_X_sub_C, coeff_divByMonic_X_sub_C_rec, degree_add_divByMonic, degree_divByMonic_le, degree_divByMonic_lt, degree_eq_one_of_irreducible_of_root, degree_modByMonic_le, degree_modByMonic_le_left, degree_modByMonic_lt, divByMonic_eq_of_not_monic, divByMonic_eq_zero_iff, divByMonic_one, divByMonic_zero, div_modByMonic_unique, div_wf_lemma, dvd_iff_isRoot, eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le, eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le, eq_of_dvd_of_natDegree_le_of_leadingCoeff, eq_of_monic_of_dvd_of_natDegree_le, eval_divByMonic_eq_trailingCoeff_comp, eval_divByMonic_pow_rootMultiplicity_ne_zero, eval₂_modByMonic_eq_self_of_root, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, finiteMultiplicity_X_sub_C, finiteMultiplicity_of_degree_pos_of_monic, le_rootMultiplicity_iff, le_rootMultiplicity_mul, leadingCoeff_divByMonic_X_sub_C, leadingCoeff_divByMonic_of_monic, map_divByMonic, map_dvd_map, map_modByMonic, map_mod_divByMonic, modByMonic_X, modByMonic_X_sub_C_eq_C_eval, modByMonic_add_div, modByMonic_eq_of_dvd_sub, modByMonic_eq_of_not_monic, modByMonic_eq_self_iff, modByMonic_eq_sub_mul_div, modByMonic_eq_zero_iff_dvd, modByMonic_one, modByMonic_zero, mul_divByMonic_cancel_left, mul_divByMonic_eq_iff_isRoot, mul_modByMonic, mul_self_modByMonic, natDegree_divByMonic, natDegree_modByMonic_le, natDegree_modByMonic_le_left, natDegree_modByMonic_lt, neg_modByMonic, not_isField, pow_mul_divByMonic_rootMultiplicity_eq, pow_rootMultiplicity_dvd, pow_rootMultiplicity_not_dvd, rootMultiplicity_C, rootMultiplicity_add, rootMultiplicity_eq_multiplicity, rootMultiplicity_eq_natFind_of_ne_zero, rootMultiplicity_eq_natTrailingDegree', rootMultiplicity_eq_nat_find_of_nonzero, rootMultiplicity_eq_zero, rootMultiplicity_eq_zero_iff, rootMultiplicity_le_iff, rootMultiplicity_le_rootMultiplicity_of_dvd, rootMultiplicity_pos, rootMultiplicity_pos', rootMultiplicity_zero, self_mul_modByMonic, sub_dvd_eval_sub, sub_modByMonic, sum_modByMonic_coeff, zero_divByMonic, zero_modByMonic	88
Total	95

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRoot_eq_bot_of_natDegree_ne_one 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.IsRoot Bot.bot Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	le_bot_iff not_isRoot_of_natDegree_ne_one
not_isRoot_of_natDegree_ne_one 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.IsRoot	—	Polynomial.natDegree_eq_of_degree_eq_some Polynomial.degree_eq_one_of_irreducible_of_root
subsingleton_isRoot 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Set.Subsingleton setOf Polynomial.IsRoot	—	Polynomial.subsingleton_isRoot_of_natDegree_eq_one Polynomial.natDegree_eq_of_degree_eq_some Polynomial.degree_eq_one_of_irreducible_of_root

Polynomial

Definitions

Name	Category	Theorems
decidableDvdMonic 📖	CompOp	—
divByMonic 📖	CompOp	35 math math: mul_divByMonic_cancel_left, mul_divByMonic_eq_iff_isRoot, div_def, divByMonic_eq_of_not_monic, isCoprime_of_is_root_of_eval_derivative_ne_zero, coeff_divByMonic_X_sub_C_rec, divByMonic_eq_zero_iff, eval_divByMonic_eq_trailingCoeff_comp, natDegree_divByMonic, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, zero_divByMonic, isUnit_iff', degreeLT.addLinearEquiv_apply_snd, X_sub_C_mul_divByMonic_eq_sub_modByMonic, modByMonic_eq_sub_mul_div, degreeLT.addLinearEquiv_apply, degree_divByMonic_le, eval_iterate_derivative_rootMultiplicity, degreeLT.addLinearEquiv_apply', div_modByMonic_unique, leadingCoeff_divByMonic_of_monic, divByMonic_eq_div, divByMonic_zero, degree_add_divByMonic, modByMonic_add_div, coeff_divByMonic_mem_pow_natDegree_mul, degree_divByMonic_lt, pow_mul_divByMonic_rootMultiplicity_eq, map_divByMonic, cyclotomic_eq_X_pow_sub_one_div, coeff_divByMonic_X_sub_C, leadingCoeff_divByMonic_X_sub_C, divByMonic_one, map_mod_divByMonic, cyclotomic'_eq_X_pow_sub_one_div
divModByMonicAux 📖	CompOp	1 math math: coeff_divModByMonicAux_mem_span_pow_mul_span
modByMonic 📖	CompOp	48 math math: modByMonic_eq_self_iff, Matrix.pow_eq_aeval_mod_charpoly, map_modByMonic, modByMonic_one, natDegree_modByMonic_le, degreeLT.addLinearEquiv_apply_fst, modByMonic_eq_of_not_monic, modByMonic_eq_zero_iff_quotient_eq_zero, IsAdjoinRootMonic.map_modByMonic, degree_modByMonic_le, modByMonicHom_apply, X_sub_C_mul_divByMonic_eq_sub_modByMonic, modByMonic_eq_zero_iff_dvd, idealSpan_range_update_divByMonic, LinearMap.pow_eq_aeval_mod_charpoly, IsAdjoinRootMonic.modByMonicHom_map, coeff_modByMonic_mem_pow_natDegree_mul, natDegree_modByMonic_lt, aeval_modByMonic_eq_self_of_root, modByMonic_eq_sub_mul_div, degreeLT.addLinearEquiv_apply, neg_modByMonic, self_mul_modByMonic, AdjoinRoot.modByMonicHom_mk, modByMonic_zero, degreeLT.addLinearEquiv_apply', LinearMap.aeval_eq_aeval_mod_charpoly, mul_self_modByMonic, div_modByMonic_unique, sub_modByMonic, modByMonic_X_sub_C_eq_C_eval, degree_modByMonic_lt, eval₂_modByMonic_eq_self_of_root, modByMonic_add_div, modByMonic_eq_of_dvd_sub, natDegree_modByMonic_le_left, modByMonic_X, sum_modByMonic_coeff, smul_modByMonic, add_modByMonic, zero_modByMonic, mul_modByMonic, Matrix.aeval_eq_aeval_mod_charpoly, mod_def, degree_modByMonic_le_left, map_mod_divByMonic, IsAdjoinRootMonic.modByMonic_repr_map, modByMonic_eq_mod
rootMultiplicity 📖	CompOp	58 math math: pow_rootMultiplicity_dvd, rootMultiplicity_eq_rootMultiplicity, rootMultiplicity_eq_natTrailingDegree, eq_rootMultiplicity_map, rootMultiplicity_scaleRoots, rootMultiplicity_eq_natTrailingDegree', rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero, rootMultiplicity_expand_pow, rootMultiplicity_sub_one_le_derivative_rootMultiplicity, count_map_roots, eval_divByMonic_eq_trailingCoeff_comp, rootMultiplicity_eq_zero_iff, rootMultiplicity_X_sub_C_pow, derivative_rootMultiplicity_of_root, pow_rootMultiplicity_not_dvd, le_rootMultiplicity_map, rootMultiplicity_mul, prod_multiset_root_eq_finset_root, rootMultiplicity_eq_natFind_of_ne_zero, LinearMap.finrank_genEigenspace_le, rootMultiplicity_eq_nat_find_of_nonzero, count_map_roots_of_injective, rootMultiplicity_add, le_rootMultiplicity_iff, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors, rootMultiplicity_mul_X_sub_C_pow, count_roots, rootMultiplicity_pos, lt_rootMultiplicity_iff_isRoot_iterate_derivative, exists_multiset_roots, eval_iterate_derivative_rootMultiplicity, rootMultiplicity_C, natDegree_hilbertPoly_of_ne_zero, Chebyshev.rootMultiplicity_T_real, rootMultiplicity_le_one_of_separable, rootMultiplicity_expand, exists_eq_pow_rootMultiplicity_mul_and_not_dvd, one_lt_rootMultiplicity_iff_isRoot_gcd, Chebyshev.rootMultiplicity_U_real, rootMultiplicity_le_rootMultiplicity_of_dvd, rootMultiplicity_eq_multiplicity, rootMultiplicity_le_iff, rootMultiplicity_eq_zero, lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors, rootMultiplicity_mul', rootMultiplicity_X_sub_C_self, one_lt_rootMultiplicity_iff_isRoot_iterate_derivative, rootMultiplicity_X_sub_C, pow_mul_divByMonic_rootMultiplicity_eq, rootMultiplicity_zero, LinearMap.finrank_maxGenEigenspace_eq, le_rootMultiplicity_mul, rootMultiplicity_pos', one_lt_rootMultiplicity_iff_isRoot, lt_rootMultiplicity_of_isRoot_iterate_derivative, lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors', LinearMap.finrank_eigenspace_le, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
«term_%ₘ_» 📖	CompOp	—
«term_/ₘ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_dvd_iff 📖	mathematical	—	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring X coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	coeff_X_mul_zero add_zero C_0 X_mul_divX_add
X_dvd_sub_C 📖	mathematical	—	Polynomial Ring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring X instSub DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C coeff	—	coeff_sub coeff_C sub_self
X_pow_dvd_iff 📖	mathematical	—	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	coeff_X_pow_mul' not_le_of_gt instIsEmptyFalse pow_zero coeff_X_pow_mul X_dvd_iff zero_add pow_succ mul_assoc
X_sub_C_dvd_sub_C_eval 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval	—	dvd_iff_isRoot IsRoot.eq_1 eval_sub eval_C sub_self
add_modByMonic 📖	mathematical	—	modByMonic CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd Ring.toSemiring	—	subsingleton_or_nontrivial Unique.instSubsingleton div_modByMonic_unique mul_add Distrib.leftDistribClass add_left_comm add_assoc modByMonic_add_div add_comm LE.le.trans_lt degree_add_le max_lt degree_modByMonic_lt modByMonic_eq_of_not_monic
associated_of_dvd_of_degree_eq 📖	mathematical	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Field.toCommRing degree	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Associated.refl associated_of_dvd_of_natDegree_le natDegree_le_natDegree Eq.ge
associated_of_dvd_of_natDegree_le 📖	mathematical	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Field.toCommRing natDegree	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	associated_of_dvd_of_natDegree_le_of_leadingCoeff instIsDomain IsUnit.dvd isUnit_iff_ne_zero leadingCoeff_ne_zero
associated_of_dvd_of_natDegree_le_of_leadingCoeff 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing natDegree leadingCoeff	Associated MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	associated_of_dvd_dvd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero leadingCoeff_mul IsDomain.to_noZeroDivisors eq_of_dvd_of_natDegree_le_of_leadingCoeff Units.mul_right_dvd natDegree_mul_C IsDomain.toNontrivial leadingCoeff_C
coeff_divByMonic_X_sub_C 📖	mathematical	—	coeff Ring.toSemiring divByMonic Polynomial instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.Icc Nat.instPreorder Nat.instLocallyFiniteOrder natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finset.Icc_eq_empty LT.lt.not_ge Finset.sum_empty Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim divByMonic_eq_zero_iff monic_X_sub_C degree_lt_degree natDegree_X_sub_C Nat.instZeroLEOneClass coeff_zero coeff_eq_zero_of_natDegree_lt natDegree_divByMonic LT.lt.trans_le Finset.left_notMem_Ioc Finset.Icc_eq_cons_Ioc Finset.sum_cons pow_zero one_mul Finset.mul_sum Finset.sum_congr Finset.ext Nat.instNoMaxOrder mul_assoc pow_succ' add_comm Finset.mem_Icc le_of_not_ge le_rfl
coeff_divByMonic_X_sub_C_rec 📖	mathematical	—	coeff Ring.toSemiring divByMonic Polynomial instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim monic_X_sub_C modByMonic_add_div LT.lt.trans_le degree_modByMonic_lt degree_X_sub_C WithBot.coe_le_coe le_add_self Nat.instCanonicallyOrderedAdd sub_mul add_sub coeff_sub coeff_add coeff_eq_zero_of_degree_lt coeff_X_mul zero_add coeff_C_mul sub_add_cancel
degree_add_divByMonic 📖	mathematical	Monic Ring.toSemiring WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree	WithBot.add divByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim degree_of_subsingleton WithBot.add_bot divByMonic_eq_zero_iff not_lt Monic.def one_mul leadingCoeff_eq_zero degree_modByMonic_lt degree_mul' degree_eq_natDegree Monic.ne_zero Nat.cast_add Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero degree_add_eq_right_of_degree_lt modByMonic_add_div
degree_divByMonic_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Ring.toSemiring divByMonic	—	zero_divByMonic degree_add_divByMonic degree_eq_natDegree Monic.ne_zero Nontrivial.of_polynomial_ne divByMonic_eq_zero_iff not_lt WithBot.coe_le_coe div_wf_lemma divModByMonicAux.eq_def bot_le divByMonic_eq_of_not_monic
degree_divByMonic_lt 📖	mathematical	Monic Ring.toSemiring WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	divByMonic	—	divByMonic_eq_zero_iff Nontrivial.of_polynomial_ne degree_eq_natDegree WithBot.bot_lt_coe degree_add_divByMonic not_lt Monic.ne_zero Nat.cast_lt WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero Nat.cast_zero Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial WithBot.instIsOrderedRing IsStrictOrderedRing.toIsOrderedRing WithBot.nontrivial
degree_eq_one_of_irreducible_of_root 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring IsRoot	degree WithBot WithBot.one Nat.instOne	—	dvd_iff_isRoot Irreducible.isUnit_or_isUnit degree_X_sub_C IsDomain.toNontrivial degree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors degree_mul add_zero
degree_modByMonic_le 📖	mathematical	Monic Ring.toSemiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim degree_of_subsingleton LT.lt.le degree_modByMonic_lt
degree_modByMonic_le_left 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Ring.toSemiring modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim degree_of_subsingleton lt_or_ge modByMonic_eq_self_iff le_refl LE.le.trans degree_modByMonic_le modByMonic_eq_of_not_monic
degree_modByMonic_lt 📖	mathematical	Monic Ring.toSemiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree modByMonic	—	—
divByMonic_eq_of_not_monic 📖	mathematical	Monic Ring.toSemiring	divByMonic Polynomial instZero	—	—
divByMonic_eq_zero_iff 📖	mathematical	Monic Ring.toSemiring	divByMonic Polynomial instZero WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	modByMonic_add_div modByMonic_eq_self_iff add_zero MulZeroClass.mul_zero not_le_of_gt div_wf_lemma divModByMonicAux.eq_def
divByMonic_one 📖	mathematical	—	divByMonic Polynomial Ring.toSemiring instOne	—	modByMonic_add_div monic_one modByMonic_one one_mul zero_add
divByMonic_zero 📖	mathematical	—	divByMonic Polynomial Ring.toSemiring instZero	—	Unique.instSubsingleton monic_zero_iff_subsingleton div_wf_lemma divModByMonicAux.eq_def
div_modByMonic_unique 📖	mathematical	Monic Ring.toSemiring Polynomial instAdd instMul WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	divByMonic modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton eq_of_sub_eq_zero sub_eq_zero_of_eq modByMonic_add_div sub_eq_add_neg mul_add Distrib.leftDistribClass neg_mul mul_neg neg_neg neg_add_rev add_comm add_left_comm add_assoc degree_neg degree_sub_le max_lt_iff degree_modByMonic_lt by_contradiction not_le_of_gt degree_eq_natDegree Monic.ne_zero WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero degree_mul' Monic.def one_mul MulZeroClass.mul_zero
div_wf_lemma 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Ring.toSemiring Monic	Preorder.toLT Polynomial instSub instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X natDegree	—	leadingCoeff_eq_zero Monic.ne_zero_of_polynomial_ne Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero degree_eq_natDegree degree_sub_lt Monic.degree_mul_comm Monic.degree_mul degree_C_mul_X_pow Nat.cast_add tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.instOrderedSub leadingCoeff_monic_mul leadingCoeff_mul_X_pow leadingCoeff_C
dvd_iff_isRoot 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C IsRoot	—	C_0 modByMonic_X_sub_C_eq_C_eval modByMonic_eq_zero_iff_dvd monic_X_sub_C mul_divByMonic_eq_iff_isRoot
eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le 📖	mathematical	Monic CommSemiring.toSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring natDegree	instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff	—	mul_comm eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le
eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le 📖	mathematical	Monic Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring natDegree	instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C leadingCoeff	—	eq_or_ne MulZeroClass.mul_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Monic.natDegree_mul' IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd eq_C_of_natDegree_eq_zero leadingCoeff_monic_mul leadingCoeff_C
eq_of_dvd_of_natDegree_le_of_leadingCoeff 📖	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing natDegree leadingCoeff	—	—	eq_or_ne LE.le.antisymm natDegree_le_of_dvd IsDomain.to_noZeroDivisors eq_C_of_natDegree_eq_zero left_eq_add AddLeftCancelSemigroup.toIsLeftCancelAdd natDegree_mul mul_ne_zero_iff instNoZeroDivisors mul_eq_left₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero leadingCoeff_ne_zero leadingCoeff_C leadingCoeff_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
eq_of_monic_of_dvd_of_natDegree_le 📖	—	Monic Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring natDegree	—	—	eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le Monic.leadingCoeff map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
eval_divByMonic_eq_trailingCoeff_comp 📖	mathematical	—	eval Ring.toSemiring CommRing.toRing divByMonic Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C rootMultiplicity trailingCoeff comp instAdd	—	eq_or_ne zero_divByMonic eval_zero zero_comp trailingCoeff_zero pow_mul_divByMonic_rootMultiplicity_eq coeff_zero_eq_eval_zero eval_comp eval_add eval_X eval_C zero_add mul_comp pow_comp sub_comp X_comp C_comp add_sub_cancel_right reverse_leadingCoeff reverse_X_pow_mul trailingCoeff.eq_1 natTrailingDegree_le_of_ne_zero eval_divByMonic_pow_rootMultiplicity_ne_zero
eval_divByMonic_pow_rootMultiplicity_ne_zero 📖	—	—	—	—	IsRoot.eq_1 dvd_iff_isRoot pow_mul_divByMonic_rootMultiplicity_eq FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt finiteMultiplicity_of_degree_pos_of_monic degree_X_sub_C Nontrivial.of_polynomial_ne monic_X_sub_C dvd_of_mul_right_eq rootMultiplicity_eq_multiplicity pow_succ mul_assoc
eval₂_modByMonic_eq_self_of_root 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	modByMonic CommRing.toRing	—	modByMonic_eq_sub_mul_div eval₂_sub eval₂_mul MulZeroClass.zero_mul sub_zero
exists_eq_pow_rootMultiplicity_mul_and_not_dvd 📖	mathematical	—	Polynomial Ring.toSemiring instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C rootMultiplicity semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring	—	rootMultiplicity_eq_multiplicity FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd finiteMultiplicity_X_sub_C
finiteMultiplicity_X_sub_C 📖	mathematical	—	FiniteMultiplicity Polynomial Ring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	finiteMultiplicity_of_degree_pos_of_monic degree_X_sub_C Nontrivial.of_polynomial_ne monic_X_sub_C
finiteMultiplicity_of_degree_pos_of_monic 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree Monic	FiniteMultiplicity Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	zero_ne_one NeZero.one Nontrivial.of_polynomial_ne MulZeroClass.mul_zero one_pow leadingCoeff_pow' one_mul Nat.cast_lt WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero degree_eq_natDegree ne_of_lt lt_add_of_le_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd le_mul_of_one_le_right IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing add_pos_of_pos_of_nonneg add_assoc add_mul Distrib.rightDistribClass natDegree_pow' natDegree_mul'
le_rootMultiplicity_iff 📖	mathematical	—	rootMultiplicity CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	finiteMultiplicity_X_sub_C pow_zero one_dvd Dvd.dvd.trans pow_dvd_pow
le_rootMultiplicity_mul 📖	mathematical	—	rootMultiplicity CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul	—	le_rootMultiplicity_iff pow_add mul_dvd_mul pow_rootMultiplicity_dvd
leadingCoeff_divByMonic_X_sub_C 📖	mathematical	—	leadingCoeff Ring.toSemiring CommRing.toRing divByMonic Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Ne.lt_or_gt degree_eq_bot Nat.WithBot.lt_zero_iff zero_divByMonic leadingCoeff_divByMonic_of_monic monic_X_sub_C degree_X_sub_C IsDomain.toNontrivial Nat.WithBot.one_le_iff_zero_lt
leadingCoeff_divByMonic_of_monic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree	leadingCoeff Ring.toSemiring CommRing.toRing divByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Monic.leadingCoeff one_mul divByMonic_eq_zero_iff modByMonic_add_div leadingCoeff_add_of_degree_lt degree_mul' degree_add_divByMonic LT.lt.trans_le degree_modByMonic_lt leadingCoeff_monic_mul
map_divByMonic 📖	mathematical	Monic Ring.toSemiring	map divByMonic	—	map_mod_divByMonic
map_dvd_map 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike Monic	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring map	—	modByMonic_eq_zero_iff_dvd Monic.map map_modByMonic map_injective map_zero
map_modByMonic 📖	mathematical	Monic Ring.toSemiring	map modByMonic	—	map_mod_divByMonic
map_mod_divByMonic 📖	mathematical	Monic Ring.toSemiring	map divByMonic modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton div_modByMonic_unique Monic.map map_mul map_add modByMonic_add_div degree_map_le degree_modByMonic_lt RingHom.domain_nontrivial degree_map_eq_of_leadingCoeff_ne_zero Monic.def RingHom.map_one one_ne_zero NeZero.one
modByMonic_X 📖	mathematical	—	modByMonic CommRing.toRing X Ring.toSemiring DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	modByMonic_X_sub_C_eq_C_eval C_0 sub_zero
modByMonic_X_sub_C_eq_C_eval 📖	mathematical	—	modByMonic CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton modByMonic_eq_sub_mul_div monic_X_sub_C eval_sub eval_mul eval_X eval_C sub_self MulZeroClass.zero_mul sub_zero degree_modByMonic_lt degree_X_sub_C bot_le WithBot.coe_le_coe WithBot.coe_lt_coe eq_C_of_degree_le_zero
modByMonic_add_div 📖	mathematical	Monic Ring.toSemiring	Polynomial instAdd modByMonic instMul divByMonic	—	eq_sub_iff_add_eq modByMonic_eq_sub_mul_div
modByMonic_eq_of_dvd_sub 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing instSub CommRing.toRing	modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton div_modByMonic_unique sub_eq_iff_eq_add mul_add Distrib.leftDistribClass add_assoc modByMonic_add_div add_comm degree_modByMonic_lt
modByMonic_eq_of_not_monic 📖	mathematical	Monic Ring.toSemiring	modByMonic	—	—
modByMonic_eq_self_iff 📖	mathematical	Monic Ring.toSemiring	modByMonic WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	degree_modByMonic_lt not_le_of_gt div_wf_lemma divModByMonicAux.eq_def
modByMonic_eq_sub_mul_div 📖	mathematical	Monic Ring.toSemiring	modByMonic Polynomial instSub instMul divByMonic	—	—
modByMonic_eq_zero_iff_dvd 📖	mathematical	Monic Ring.toSemiring	modByMonic Polynomial instZero semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring	—	modByMonic_add_div zero_add dvd_mul_right Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton exists_eq_mul_right_of_dvd modByMonic_eq_sub_mul_div mul_sub degree_modByMonic_lt leadingCoeff_eq_zero MulZeroClass.mul_zero leadingCoeff_zero Monic.def one_mul not_lt_of_ge WithBot.coe_lt_coe degree_eq_natDegree Monic.ne_zero degree_mul'
modByMonic_one 📖	mathematical	—	modByMonic Polynomial Ring.toSemiring instOne instZero	—	modByMonic_eq_zero_iff_dvd monic_one one_dvd
modByMonic_zero 📖	mathematical	—	modByMonic Polynomial Ring.toSemiring instZero	—	Unique.instSubsingleton monic_zero_iff_subsingleton div_wf_lemma divModByMonicAux.eq_def
mul_divByMonic_cancel_left 📖	mathematical	Monic Ring.toSemiring	divByMonic Polynomial instMul	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton div_modByMonic_unique zero_add degree_zero Ne.bot_lt Monic.ne_zero degree_eq_bot
mul_divByMonic_eq_iff_isRoot 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring CommRing.toRing instMul instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C divByMonic IsRoot	—	eval_mul eval_sub eval_X eval_C sub_self MulZeroClass.zero_mul modByMonic_add_div monic_X_sub_C modByMonic_X_sub_C_eq_C_eval C_0 zero_add IsRoot.def
mul_modByMonic 📖	mathematical	—	modByMonic CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul Ring.toSemiring	—	modByMonic_eq_of_not_monic modByMonic_eq_of_dvd_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_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_congr Mathlib.Tactic.Ring.add_pf_add_gt 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 dvd_add Distrib.leftDistribClass dvd_mul_of_dvd_right modByMonic_eq_sub_mul_div sub_sub_cancel
mul_self_modByMonic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	modByMonic CommRing.toRing Polynomial instMul Ring.toSemiring instZero	—	modByMonic_eq_zero_iff_dvd dvd_mul_left
natDegree_divByMonic 📖	mathematical	Monic Ring.toSemiring	natDegree divByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub natDegree_zero tsub_eq_zero_iff_le natDegree_le_natDegree le_of_lt divByMonic_eq_zero_iff degree_add_divByMonic zero_divByMonic WithBot.charZero Nat.instCharZero Nat.cast_add degree_eq_natDegree Monic.ne_zero add_tsub_cancel_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
natDegree_modByMonic_le 📖	mathematical	Monic Ring.toSemiring	natDegree modByMonic	—	natDegree_le_natDegree degree_modByMonic_le
natDegree_modByMonic_le_left 📖	mathematical	—	natDegree Ring.toSemiring modByMonic	—	natDegree_le_natDegree degree_modByMonic_le_left
natDegree_modByMonic_lt 📖	mathematical	Monic Ring.toSemiring	natDegree modByMonic	—	natDegree_zero Mathlib.Tactic.Contrapose.contrapose₄ eq_one_of_monic_natDegree_zero natDegree_lt_natDegree degree_modByMonic_lt Nontrivial.of_polynomial_ne
neg_modByMonic 📖	mathematical	—	modByMonic CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instNeg Ring.toSemiring	—	eq_neg_iff_add_eq_zero add_modByMonic neg_add_cancel zero_modByMonic
not_isField 📖	mathematical	—	IsField Polynomial Ring.toSemiring semiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton natDegree_X natDegree_one Monic.eq_one_of_isUnit monic_X Ne.isUnit Monic.ne_zero
pow_mul_divByMonic_rootMultiplicity_eq 📖	mathematical	—	Polynomial Ring.toSemiring instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C rootMultiplicity divByMonic	—	Monic.pow monic_X_sub_C modByMonic_add_div modByMonic_eq_zero_iff_dvd pow_rootMultiplicity_dvd zero_add
pow_rootMultiplicity_dvd 📖	mathematical	—	Polynomial Ring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C rootMultiplicity	—	rootMultiplicity_zero pow_zero rootMultiplicity_eq_multiplicity pow_multiplicity_dvd
pow_rootMultiplicity_not_dvd 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C rootMultiplicity	—	rootMultiplicity_le_iff le_refl
rootMultiplicity_C 📖	mathematical	—	rootMultiplicity DFunLike.coe RingHom Polynomial Ring.toSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	subsingleton_or_nontrivial Unique.instSubsingleton rootMultiplicity_zero rootMultiplicity_eq_multiplicity natDegree_C natDegree_sub_C natDegree_X Nat.instZeroLEOneClass multiplicity_eq_zero Monic.not_dvd_of_natDegree_lt monic_X_sub_C
rootMultiplicity_add 📖	mathematical	—	rootMultiplicity CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instAdd	—	le_rootMultiplicity_iff min_pow_dvd_add pow_rootMultiplicity_dvd
rootMultiplicity_eq_multiplicity 📖	mathematical	—	rootMultiplicity Polynomial Ring.toSemiring instZero instDecidableEq multiplicity MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	finiteMultiplicity_X_sub_C ENat.some_eq_coe WithTop.untopD_coe
rootMultiplicity_eq_natFind_of_ne_zero 📖	mathematical	—	rootMultiplicity Nat.find Polynomial Ring.toSemiring semigroupDvd Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Monoid.toNatPow instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C finiteMultiplicity_X_sub_C	—	finiteMultiplicity_X_sub_C
rootMultiplicity_eq_natTrailingDegree' 📖	mathematical	—	rootMultiplicity CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing natTrailingDegree CommSemiring.toSemiring CommRing.toCommSemiring	—	rootMultiplicity_zero le_antisymm rootMultiplicity_le_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero X_pow_dvd_iff trailingCoeff_nonzero_iff_nonzero le_rootMultiplicity_iff coeff_eq_zero_of_lt_natTrailingDegree
rootMultiplicity_eq_nat_find_of_nonzero 📖	mathematical	—	rootMultiplicity Nat.find Polynomial Ring.toSemiring semigroupDvd Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Monoid.toNatPow instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C finiteMultiplicity_X_sub_C	—	rootMultiplicity_eq_natFind_of_ne_zero
rootMultiplicity_eq_zero 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring	rootMultiplicity CommRing.toRing	—	rootMultiplicity_eq_zero_iff
rootMultiplicity_eq_zero_iff 📖	mathematical	—	rootMultiplicity CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero	—	rootMultiplicity_eq_multiplicity
rootMultiplicity_le_iff 📖	mathematical	—	rootMultiplicity CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	Iff.not le_rootMultiplicity_iff not_le
rootMultiplicity_le_rootMultiplicity_of_dvd 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing	rootMultiplicity CommRing.toRing	—	le_rootMultiplicity_mul
rootMultiplicity_pos 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring	—	rootMultiplicity_pos'
rootMultiplicity_pos' 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring	—	pos_iff_ne_zero Nat.instCanonicallyOrderedAdd rootMultiplicity_eq_zero_iff
rootMultiplicity_zero 📖	mathematical	—	rootMultiplicity Polynomial Ring.toSemiring instZero	—	finiteMultiplicity_X_sub_C
self_mul_modByMonic 📖	mathematical	Monic Ring.toSemiring	modByMonic Polynomial instMul instZero	—	modByMonic_eq_zero_iff_dvd dvd_mul_right
sub_dvd_eval_sub 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing eval CommSemiring.toSemiring CommRing.toCommSemiring	—	eval_sub eval_C sub_self eval_X map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
sub_modByMonic 📖	mathematical	—	modByMonic CommRing.toRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub Ring.toSemiring	—	sub_eq_add_neg add_modByMonic neg_modByMonic
sum_modByMonic_coeff 📖	mathematical	Monic Ring.toSemiring WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ring Finset.univ Fin.fintype DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial coeff modByMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton sum_fin monomial_zero_right LT.lt.trans_le degree_modByMonic_lt sum_monomial_eq
zero_divByMonic 📖	mathematical	—	divByMonic Polynomial Ring.toSemiring instZero	—	—
zero_modByMonic 📖	mathematical	—	modByMonic Polynomial Ring.toSemiring instZero	—	—

Polynomial.IsRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_coeff_zero 📖	mathematical	Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.coeff	—	Polynomial.coeff_zero_eq_eval_zero zero_sub eq_zero sub_zero Polynomial.sub_dvd_eval_sub

---

← Back to Index