FieldDivision

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

Statistics

Metric	Count
Definitions div, instDiv, instEuclideanDomain, instMod, instNormalizationMonoid	5
Theorems degree_pos, natDegree_pos, C_div, C_mul_dvd, mul_div_eq, normalize_eq_self, X_eq_normalize, X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic, X_sub_C_mul_divByMonic_eq_sub_modByMonic, add_mod, coe_normUnit, coe_normUnit_of_ne_zero, coeff_inv_units, degree_add_div, degree_div_le, degree_div_lt, degree_map, degree_mod_lt, degree_normalize, degree_pos_of_irreducible, degree_pos_of_ne_zero_of_nonunit, derivative_rootMultiplicity_of_root, derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors, divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative, divByMonic_eq_div, div_C, div_C_mul, div_def, div_eq_zero_iff, dvd_C_mul, eval_gcd_eq_zero, eval_iterate_derivative_rootMultiplicity, eval₂_gcd_eq_zero, exists_root_of_degree_eq_one, gcd_map, irreducible_iff_degree_lt, irreducible_iff_lt_natDegree_lt, irreducible_of_degree_eq_one, isCoprime_map, isCoprime_of_is_root_of_eval_derivative_ne_zero, isRoot_gcd_iff_isRoot_left_right, isRoot_iterate_derivative_of_lt_rootMultiplicity, isRoot_of_isRoot_of_dvd_derivative_mul, isUnit_iff_degree_eq_zero, isUnit_map, leadingCoeff_div, leadingCoeff_map, leadingCoeff_mul_prod_normalizedFactors, leadingCoeff_normalize, lt_rootMultiplicity_iff_isRoot_iterate_derivative, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors, lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors', lt_rootMultiplicity_of_isRoot_iterate_derivative, lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors, lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors', map_div, map_dvd_map', map_eq_zero, map_mod, map_ne_zero, map_normalize, mem_normalizedFactors_iff, mem_roots_map, modByMonic_eq_mod, mod_X_sub_C_eq_C_eval, mod_def, mod_eq_of_dvd_sub, mod_eq_self_iff, monic_mapAlg_iff, monic_map_iff, monic_normalize, mul_div_eq_iff_isRoot, mul_mod, natDegree_map, natDegree_mod_lt, nextCoeff_map_eq, normUnit_X, normalize_eq_self_iff_monic, not_irreducible_C, one_lt_rootMultiplicity_iff_isRoot, one_lt_rootMultiplicity_iff_isRoot_gcd, one_lt_rootMultiplicity_iff_isRoot_iterate_derivative, prime_of_degree_eq_one, rootMultiplicity_sub_one_le_derivative_rootMultiplicity, rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero, rootSet_C_mul_X_pow, rootSet_X_pow, rootSet_monomial, rootSet_prod, root_gcd_iff_root_left_right, root_left_of_root_gcd, root_right_of_root_gcd, roots_C_mul_X_add_C, roots_C_mul_X_sub_C, roots_degree_eq_one, roots_normalize, sub_mod	97
Total	102

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_pos 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Polynomial.degree	—	Polynomial.natDegree_pos_iff_degree_pos natDegree_pos
natDegree_pos 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.natDegree	—	Polynomial.natDegree_eq_zero not_irreducible_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass not_isUnit Polynomial.isUnit_C Ne.isUnit

Polynomial

Definitions

Name	Category	Theorems
div 📖	CompOp	—
instDiv 📖	CompOp	21 math math: mul_div_eq_iff_isRoot, degree_add_div, RatFunc.num_div, div_def, map_div, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, AdjoinRoot.mul_div_root_cancel, RatFunc.numDenom_div, Lagrange.basis_eq_prod_sub_inv_mul_nodal_div, IsRoot.mul_div_eq, div_eq_zero_iff, RatFunc.denom_div, div_C, C_div, divByMonic_eq_div, RatFunc.num_div_dvd', degree_div_lt, leadingCoeff_div, degree_div_le, div_C_mul, Lagrange.nodal_erase_eq_nodal_div
instEuclideanDomain 📖	CompOp	34 math math: splits_of_splits_gcd_right, abc, splits_of_splits_gcd_left, valuation_of_mk, cardPowDegree_isEuclidean, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, PowerSeries.intValuation_eq_of_coe, divRadical_dvd_derivative, leadingCoeff_mul_prod_normalizedFactors, PowerSeries.normalized_count_X_eq_of_coe, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, RatFunc.valuation_eq_LaurentSeries_valuation, isRoot_gcd_iff_isRoot_left_right, natDegree_radical_le, gcd_map, RatFunc.v_def, divRadical_dvd_wronskian_right, LaurentSeries.powerSeries_ext_subring, separable_gcd_right, separable_gcd_left, LaurentSeries.powerSeriesRingEquiv_coe_apply, root_gcd_iff_root_left_right, mem_normalizedFactors_iff, Ideal.factors_span_eq, LaurentSeries.tendsto_valuation, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, eval₂_gcd_eq_zero, divRadical_dvd_wronskian_left, LaurentSeries.mem_integers_of_powerSeries, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, eval_gcd_eq_zero, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, degree_radical_le, valuation_X_eq_neg_one
instMod 📖	CompOp	14 math math: exists_partition_polynomial, mod_eq_self_iff, exists_partition_polynomial_aux, add_mod, map_mod, sub_mod, mod_eq_of_dvd_sub, exists_approx_polynomial, mul_mod, mod_X_sub_C_eq_C_eval, natDegree_mod_lt, degree_mod_lt, mod_def, modByMonic_eq_mod
instNormalizationMonoid 📖	CompOp	24 math math: degree_normalize, coe_normUnit_of_ne_zero, roots_normalize, abc, Monic.normalize_eq_self, divRadical_dvd_derivative, leadingCoeff_mul_prod_normalizedFactors, leadingCoeff_normalize, PowerSeries.normalized_count_X_eq_of_coe, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, natDegree_radical_le, divRadical_dvd_wronskian_right, normalize_eq_self_iff_monic, mem_normalizedFactors_iff, coe_normUnit, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, divRadical_dvd_wronskian_left, normUnit_X, monic_normalize, normalizedFactors_cyclotomic_card, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, X_eq_normalize, map_normalize, degree_radical_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_div 📖	mathematical	—	DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Semiring.toNonAssocSemiring semiring RingHom.instFunLike C DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing instDiv	—	div_C C_mul div_eq_mul_inv
C_mul_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	dvd_trans dvd_mul_left mul_assoc mul_left_comm RingHom.map_mul mul_inv_cancel₀ RingHom.map_one one_mul
X_eq_normalize 📖	mathematical	—	X CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid	—	normUnit_X mul_one
X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic 📖	mathematical	Polynomial Ring.toSemiring DivisionRing.toRing Field.toDivisionRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C divByMonic	LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative mul_add Distrib.leftDistribClass
X_sub_C_mul_divByMonic_eq_sub_modByMonic 📖	mathematical	—	Polynomial Ring.toSemiring instMul instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C divByMonic modByMonic	—	eq_sub_iff_add_eq eq_sub_iff_add_eq' modByMonic_eq_sub_mul_div monic_X_sub_C
add_mod 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod instAdd	—	add_modByMonic
coe_normUnit 📖	mathematical	—	Units.val Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring NormalizationMonoid.normUnit instNormalizationMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff	—	—
coe_normUnit_of_ne_zero 📖	mathematical	—	Units.val Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain commSemiring NormalizationMonoid.normUnit instNormalizationMonoid IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid leadingCoeff	—	leadingCoeff_eq_zero IsDomain.to_noZeroDivisors instIsDomain coe_normUnit CommGroupWithZero.coe_normUnit
coeff_inv_units 📖	mathematical	—	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield coeff DivisionSemiring.toSemiring Semifield.toDivisionSemiring Units.val Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Units Units.instInv	—	eq_C_of_degree_eq_zero degree_coe_units IsDomain.to_noZeroDivisors instIsDomain EuclideanDomain.toNontrivial coeff_C inv_eq_one_div div_eq_iff_mul_eq coeff_coe_units_zero_ne_zero coeff_zero_eq_eval_zero eval_mul Units.val_mul inv_mul_cancel eval_one div_zero
degree_add_div 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	WithBot.add Polynomial instDiv	—	EuclideanDomain.mod_lt degree_le_mul_left IsDomain.to_noZeroDivisors instIsDomain div_eq_zero_iff not_lt_of_ge EuclideanDomain.div_add_mod degree_add_eq_left_of_degree_lt degree_mul
degree_div_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instDiv	—	EuclideanDomain.div_zero div_def mul_comm degree_mul_leadingCoeff_inv degree_divByMonic_le
degree_div_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Polynomial instDiv	—	div_def mul_comm degree_mul_leadingCoeff_inv degree_divByMonic_lt monic_mul_leadingCoeff_inv
degree_map 📖	mathematical	—	degree map Ring.toSemiring	—	degree_map_eq_of_injective RingHom.injective
degree_mod_lt 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instMod	—	mod_def LT.lt.trans_eq degree_modByMonic_lt EuclideanDomain.toNontrivial Monic.leadingCoeff leadingCoeff_mul IsDomain.to_noZeroDivisors instIsDomain leadingCoeff_C mul_inv_cancel₀ degree_mul degree_add_degree_leadingCoeff_inv
degree_normalize 📖	mathematical	—	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero	—	IsDomain.to_noZeroDivisors instIsDomain coe_normUnit degree_mul degree_C EuclideanDomain.toNontrivial add_zero
degree_pos_of_irreducible 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	lt_of_not_ge eq_C_of_degree_le_zero not_irreducible_C
degree_pos_of_ne_zero_of_nonunit 📖	mathematical	IsUnit Polynomial DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	lt_of_not_ge eq_C_of_degree_le_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass nontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
derivative_rootMultiplicity_of_root 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring	rootMultiplicity CommRing.toRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass rootMultiplicity_zero derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors mem_nonZeroDivisors_of_ne_zero Nat.cast_ne_zero LT.lt.ne' rootMultiplicity_pos
derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing rootMultiplicity	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass rootMultiplicity_zero exists_eq_pow_rootMultiplicity_mul_and_not_dvd rootMultiplicity_pos derivative_mul dvd_add_left dvd_mul_right derivative_X_sub_C_pow pow_succ mul_comm mul_assoc dvd_cancel_left_mem_nonZeroDivisors Monic.mem_nonZeroDivisors Monic.pow monic_X_sub_C dvd_iff_isRoot IsRoot.eq_1 eval_mul eval_C mul_left_mem_nonZeroDivisors_eq_zero_iff dvd_zero le_antisymm rootMultiplicity_le_iff rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero
divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative 📖	mathematical	—	Polynomial Ring.toSemiring CommRing.toRing CommSemiring.toSemiring CommRing.toCommSemiring instAdd divByMonic instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C instMul LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	X_sub_C_mul_divByMonic_eq_sub_modByMonic derivative_mul derivative_sub derivative_X derivative_C sub_zero one_mul modByMonic_X_sub_C_eq_C_eval
divByMonic_eq_div 📖	mathematical	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	divByMonic DivisionRing.toRing Field.toDivisionRing Polynomial instDiv	—	Monic.def inv_one mul_one one_mul
div_C 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instDiv DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C instMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	mul_comm one_mul EuclideanDomain.div_one div_C_mul
div_C_mul 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instDiv instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul EuclideanDomain.div_zero inv_zero leadingCoeff_mul IsDomain.to_noZeroDivisors instIsDomain leadingCoeff_C mul_inv RingHom.map_mul mul_assoc mul_left_comm mul_inv_cancel₀ RingHom.map_one one_mul
div_def 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instDiv Ring.toSemiring DivisionRing.toRing Field.toDivisionRing instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero leadingCoeff divByMonic	—	—
div_eq_zero_iff 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instDiv instZero WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	EuclideanDomain.div_add_mod mod_eq_self_iff zero_add MulZeroClass.mul_zero degree_mul_leadingCoeff_inv monic_mul_leadingCoeff_inv div_def divByMonic_eq_zero_iff EuclideanDomain.toNontrivial
dvd_C_mul 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	mul_left_comm mul_assoc RingHom.map_mul inv_mul_cancel₀ RingHom.map_one one_mul dvd_trans dvd_mul_left
eval_gcd_eq_zero 📖	mathematical	eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq	—	eval₂_gcd_eq_zero
eval_iterate_derivative_rootMultiplicity 📖	mathematical	—	eval CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative rootMultiplicity CommRing.toRing AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.factorial Ring.toSemiring divByMonic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSub X RingHom RingHom.instFunLike C	—	pow_mul_divByMonic_rootMultiplicity_eq iterate_derivative_mul eval_finset_sum Finset.sum_eq_single_of_mem Finset.mem_range iterate_derivative_X_sub_pow eval_smul IsScalarTower.right eval_mul eval_pow Finset.mem_range_succ_iff eval_sub eval_X eval_C sub_self zero_pow smul_zero MulZeroClass.zero_mul Nat.choose_zero_right one_smul iterate_derivative_X_sub_pow_self eval_natCast nsmul_eq_mul
eval₂_gcd_eq_zero 📖	mathematical	eval₂ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq	—	EuclideanDomain.gcd_eq_gcd_ab eval₂_add eval₂_mul MulZeroClass.zero_mul zero_add
exists_root_of_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot WithBot.one Nat.instOne	IsRoot	—	instIsDomain mem_roots WithBot.zeroLEOneClass Nat.instZeroLEOneClass roots_degree_eq_one
gcd_map 📖	mathematical	—	EuclideanDomain.gcd Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instEuclideanDomain instDecidableEq map	—	EuclideanDomain.GCD.induction map_zero EuclideanDomain.gcd_zero_left EuclideanDomain.gcd_val map_mod
irreducible_iff_degree_lt 📖	mathematical	IsUnit Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Irreducible	—	irreducible_mul_leadingCoeff_inv Monic.irreducible_iff_degree_lt instIsDomain monic_mul_leadingCoeff_inv Mathlib.Tactic.Contrapose.contrapose₄ IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid natDegree_mul_leadingCoeff_inv MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial nontrivial EuclideanDomain.toNontrivial
irreducible_iff_lt_natDegree_lt 📖	mathematical	IsUnit Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Irreducible semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Mathlib.Tactic.Contrapose.contrapose₄ IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid irreducible_mul_leadingCoeff_inv Monic.irreducible_iff_lt_natDegree_lt IsDomain.to_noZeroDivisors instIsDomain monic_mul_leadingCoeff_inv natDegree_mul_leadingCoeff_inv IsUnit.dvd_mul_right isUnit_C inv_ne_zero leadingCoeff_ne_zero
irreducible_of_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot WithBot.one Nat.instOne	Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Prime.irreducible instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDomain.toIsCancelMulZero instIsDomain prime_of_degree_eq_one
isCoprime_map 📖	mathematical	—	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring map	—	EuclideanDomain.gcd_isUnit_iff gcd_map isUnit_map
isCoprime_of_is_root_of_eval_derivative_ne_zero 📖	mathematical	—	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring instSub DivisionRing.toRing Field.toDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C divByMonic Ring.toSemiring	—	EuclideanDomain.dvd_or_coprime irreducible_of_degree_eq_one degree_X_sub_C EuclideanDomain.toNontrivial Mathlib.Tactic.Contrapose.contrapose₄ X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic C_0 modByMonic_X_sub_C_eq_C_eval modByMonic_eq_zero_iff_dvd monic_X_sub_C
isRoot_gcd_iff_isRoot_left_right 📖	mathematical	—	IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq	—	root_gcd_iff_root_left_right
isRoot_iterate_derivative_of_lt_rootMultiplicity 📖	mathematical	rootMultiplicity CommRing.toRing	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	dvd_iff_isRoot Dvd.dvd.trans dvd_pow_self pow_sub_dvd_iterate_derivative_of_pow_dvd pow_rootMultiplicity_dvd
isRoot_of_isRoot_of_dvd_derivative_mul 📖	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative IsRoot	—	—	Mathlib.Tactic.Contrapose.contrapose₃ eq_C_of_derivative_eq_zero IsAddTorsionFree.of_isCancelMulZero_charZero NoZeroDivisors.to_isCancelMulZero not_isRoot_C C_ne_zero mul_ne_zero instNoZeroDivisors eval_zero instNontrivialOfCharZero rootMultiplicity_pos add_comm rootMultiplicity_mul add_zero rootMultiplicity_eq_zero derivative_rootMultiplicity_of_root
isUnit_iff_degree_eq_zero 📖	mathematical	—	IsUnit Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring degree WithBot WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	degree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors instIsDomain EuclideanDomain.toNontrivial map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_C_of_degree_le_zero isUnit_iff_dvd_one C_mul mul_inv_cancel₀ C_1
isUnit_map 📖	mathematical	—	IsUnit Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring map	—	degree_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial
leadingCoeff_div 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	leadingCoeff Polynomial instDiv DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	EuclideanDomain.div_zero div_zero div_def leadingCoeff_mul IsDomain.to_noZeroDivisors instIsDomain leadingCoeff_C leadingCoeff_divByMonic_of_monic monic_mul_leadingCoeff_inv degree_mul_leadingCoeff_inv mul_comm div_eq_mul_inv
leadingCoeff_map 📖	mathematical	—	leadingCoeff map Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	leadingCoeff_map_of_injective RingHom.injective
leadingCoeff_mul_prod_normalizedFactors 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommRing.toCommMonoid commRing EuclideanDomain.toCommRing Field.toEuclideanDomain UniqueFactorizationMonoid.normalizedFactors CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring instNormalizationMonoid IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain instEuclideanDomain	—	IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass UniqueFactorizationMonoid.normalizedFactors.congr_simp UniqueFactorizationMonoid.normalizedFactors_zero mul_one UniqueFactorizationMonoid.prod_normalizedFactors_eq normalize_apply coe_normUnit CommGroupWithZero.coe_normUnit mul_comm mul_assoc map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass inv_mul_cancel₀ map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
leadingCoeff_normalize 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid	—	coe_normUnit leadingCoeff_mul leadingCoeff_C
lt_rootMultiplicity_iff_isRoot_iterate_derivative 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	isRoot_iterate_derivative_of_lt_rootMultiplicity lt_rootMultiplicity_of_isRoot_iterate_derivative
lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.factorial	rootMultiplicity IsRoot Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	isRoot_iterate_derivative_of_lt_rootMultiplicity LE.le.trans_lt lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	rootMultiplicity IsRoot Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	isRoot_iterate_derivative_of_lt_rootMultiplicity lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
lt_rootMultiplicity_of_isRoot_iterate_derivative 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	rootMultiplicity CommRing.toRing	—	lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors mem_nonZeroDivisors_of_ne_zero Nat.cast_ne_zero ne_of_gt Nat.factorial_pos
lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.factorial	rootMultiplicity	—	Nat.cast_dvd_cast Nat.factorial_dvd_factorial eval_divByMonic_pow_rootMultiplicity_ne_zero mul_left_mem_nonZeroDivisors_eq_zero_iff mul_mem_nonZeroDivisors nsmul_eq_mul eval_iterate_derivative_rootMultiplicity
lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📖	mathematical	IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	rootMultiplicity	—	lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors Nat.cast_one Submonoid.one_mem Nat.factorial_succ Nat.cast_mul mul_mem_nonZeroDivisors le_rfl LE.le.trans
map_div 📖	mathematical	—	map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instDiv	—	EuclideanDomain.div_zero map_zero div_def map_mul map_divByMonic monic_mul_leadingCoeff_inv map_C leadingCoeff_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_dvd_map' 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain map	—	map_zero zero_dvd_iff map_eq_zero DivisionRing.isSimpleRing EuclideanDomain.toNontrivial IsDomain.to_noZeroDivisors instIsDomain normalize_dvd_iff normalize_apply coe_normUnit_of_ne_zero leadingCoeff_map map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_C map_mul map_dvd_map RingHom.injective monic_mul_leadingCoeff_inv
map_eq_zero 📖	mathematical	—	map Ring.toSemiring Polynomial instZero	—	map_eq_zero_iff RingHom.injective
map_mod 📖	mathematical	—	map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instMod	—	EuclideanDomain.mod_zero map_zero mod_def leadingCoeff_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_C map_mul map_modByMonic monic_mul_leadingCoeff_inv
map_ne_zero 📖	—	—	—	—	map_eq_zero
map_normalize 📖	mathematical	—	map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero	—	IsDomain.to_noZeroDivisors instIsDomain map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass map_zero inv_inv Units.val_inv_eq_inv_val map_mul map_C map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass leadingCoeff_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial
mem_normalizedFactors_iff 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Multiset Multiset.instMembership UniqueFactorizationMonoid.normalizedFactors CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero PrincipalIdealRing.to_uniqueFactorizationMonoid commRing instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing EuclideanDomain.to_principal_ideal_domain instEuclideanDomain Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Monic semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	IsDomain.to_noZeroDivisors instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain EuclideanDomain.toNontrivial UniqueFactorizationMonoid.zero_notMem_normalizedFactors UniqueFactorizationMonoid.mem_normalizedFactors_iff' normalize_eq_self_iff_monic
mem_roots_map 📖	mathematical	—	Multiset Multiset.instMembership roots map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mem_roots map_ne_zero DivisionRing.isSimpleRing IsDomain.toNontrivial IsRoot.eq_1 eval_map
modByMonic_eq_mod 📖	mathematical	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	modByMonic DivisionRing.toRing Field.toDivisionRing Polynomial instMod	—	Monic.def inv_one mul_one
mod_X_sub_C_eq_C_eval 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod instSub DivisionRing.toRing Field.toDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval	—	modByMonic_X_sub_C_eq_C_eval modByMonic_eq_mod monic_X_sub_C
mod_def 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod modByMonic DivisionRing.toRing Field.toDivisionRing instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero leadingCoeff	—	—
mod_eq_of_dvd_sub 📖	mathematical	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instSub DivisionRing.toRing Field.toDivisionRing	instMod	—	eq_or_ne EuclideanDomain.mod_zero modByMonic_eq_of_dvd_sub Monic.leadingCoeff leadingCoeff_mul IsDomain.to_noZeroDivisors instIsDomain leadingCoeff_C mul_inv_cancel₀ mul_comm C_mul_dvd
mod_eq_self_iff 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree	—	EuclideanDomain.mod_lt not_le_of_gt degree_mul_leadingCoeff_inv mod_def modByMonic.eq_1 monic_mul_leadingCoeff_inv div_wf_lemma divModByMonicAux.eq_def
monic_mapAlg_iff 📖	mathematical	—	Monic DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield semiring algebraOfAlgebra Algebra.id AlgHom.funLike mapAlg DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	mapAlg_eq_map DivisionRing.isSimpleRing
monic_map_iff 📖	mathematical	—	Monic map Ring.toSemiring	—	Function.Injective.monic_map_iff RingHom.injective
monic_normalize 📖	mathematical	—	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero	—	IsDomain.to_noZeroDivisors instIsDomain Monic.eq_1 leadingCoeff_normalize normalize_eq_one isUnit_iff_ne_zero leadingCoeff_eq_zero
mul_div_eq_iff_isRoot 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMul instSub DivisionRing.toRing Field.toDivisionRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C instDiv IsRoot	—	mul_divByMonic_eq_iff_isRoot divByMonic_eq_div monic_X_sub_C
mul_mod 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod instMul	—	mul_modByMonic
natDegree_map 📖	mathematical	—	natDegree map Ring.toSemiring	—	natDegree_map_eq_of_injective RingHom.injective
natDegree_mod_lt 📖	mathematical	—	natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instMod	—	leadingCoeff_ne_zero Mathlib.Tactic.Contrapose.contrapose₄ mod_def LT.lt.trans_le natDegree_modByMonic_lt monic_mul_C_of_leadingCoeff_mul_eq_one mul_inv_eq_one₀ natDegree_mul_C_eq_of_mul_eq_one inv_mul_eq_one₀ natDegree_one natDegree_mul_C_le
nextCoeff_map_eq 📖	mathematical	—	nextCoeff map Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	nextCoeff_map RingHom.injective
normUnit_X 📖	mathematical	—	NormalizationMonoid.normUnit Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero commSemiring instNormalizationMonoid X Units MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Units.instOne	—	coe_normUnit Units.val_eq_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Units.val_one normUnit_one leadingCoeff_X
normalize_eq_self_iff_monic 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IsDomain.to_noZeroDivisors instIsDomain NormalizedGCDMonoid.toNormalizationMonoid CommRing.toCommSemiring CommGroupWithZero.instNormalizedGCDMonoid Semifield.toCommGroupWithZero Monic	—	IsDomain.to_noZeroDivisors instIsDomain monic_normalize Monic.normalize_eq_self
not_irreducible_C 📖	mathematical	—	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	C_0 not_irreducible_zero Irreducible.not_isUnit isUnit_C isUnit_iff_ne_zero
one_lt_rootMultiplicity_iff_isRoot 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	one_lt_rootMultiplicity_iff_isRoot_iterate_derivative Nat.instCanonicallyOrderedAdd
one_lt_rootMultiplicity_iff_isRoot_gcd 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring GCDMonoid.gcd Polynomial CommSemiring.toCommMonoidWithZero commSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	one_lt_rootMultiplicity_iff_isRoot
one_lt_rootMultiplicity_iff_isRoot_iterate_derivative 📖	mathematical	—	rootMultiplicity CommRing.toRing IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors Nat.factorial_one Nat.cast_one Submonoid.one_mem
prime_of_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot WithBot.one Nat.instOne	Prime Polynomial CommSemiring.toCommMonoidWithZero commSemiring Semifield.toCommSemiring	—	IsDomain.to_noZeroDivisors instIsDomain Monic.prime_of_degree_eq_one degree_normalize monic_normalize Associated.prime normalize_associated
rootMultiplicity_sub_one_le_derivative_rootMultiplicity 📖	mathematical	—	rootMultiplicity CommRing.toRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	Eq.le derivative_rootMultiplicity_of_root rootMultiplicity_eq_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub zero_le
rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero 📖	mathematical	—	rootMultiplicity CommRing.toRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	le_rootMultiplicity_iff pow_sub_one_dvd_derivative_of_pow_dvd pow_rootMultiplicity_dvd
rootSet_C_mul_X_pow 📖	mathematical	—	rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	C_mul_X_pow_eq_monomial rootSet_monomial
rootSet_X_pow 📖	mathematical	—	rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	one_mul C_1 rootSet_C_mul_X_pow one_ne_zero NeZero.one EuclideanDomain.toNontrivial
rootSet_monomial 📖	mathematical	—	rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	rootSet.eq_1 aroots_monomial instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Multiset.toFinset_nsmul Multiset.toFinset_singleton Finset.coe_singleton
rootSet_prod 📖	mathematical	—	rootSet EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.prod Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommMonoid commRing Set.iUnion Finset Finset.instMembership	—	Set.iUnion_congr_Prop map_prod roots_prod map_eq_zero DivisionRing.isSimpleRing IsDomain.toNontrivial Finset.bind_toFinset Finset.val_toFinset Finset.coe_biUnion
root_gcd_iff_root_left_right 📖	mathematical	—	eval₂ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	root_left_of_root_gcd root_right_of_root_gcd eval₂_gcd_eq_zero
root_left_of_root_gcd 📖	—	eval₂ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	EuclideanDomain.gcd_dvd_left eval₂_mul MulZeroClass.zero_mul
root_right_of_root_gcd 📖	—	eval₂ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	EuclideanDomain.gcd_dvd_right eval₂_mul MulZeroClass.zero_mul
roots_C_mul_X_add_C 📖	mathematical	—	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X Multiset Multiset.instSingleton NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	instIsDomain roots_C_mul_X_add_C_of_IsUnit mul_inv_cancel₀ inv_mul_cancel₀
roots_C_mul_X_sub_C 📖	mathematical	—	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSub DivisionRing.toRing Field.toDivisionRing instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X Multiset Multiset.instSingleton Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	instIsDomain roots_C_mul_X_sub_C_of_IsUnit mul_inv_cancel₀ inv_mul_cancel₀
roots_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot WithBot.one Nat.instOne	roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Multiset Multiset.instSingleton NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero coeff	—	instIsDomain eq_X_add_C_of_degree_le_one le_refl coeff_ne_zero_of_eq_degree roots_C_mul_X_add_C coeff_add coeff_mul_X coeff_C_zero coeff_C_succ add_zero mul_coeff_zero coeff_X_zero MulZeroClass.mul_zero zero_add
roots_normalize 📖	mathematical	—	roots DFunLike.coe MonoidWithZeroHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero commSemiring MonoidWithZeroHom.funLike normalize instNormalizationMonoid IsDomain.to_noZeroDivisors	—	IsDomain.to_noZeroDivisors normalize_apply mul_comm coe_normUnit roots_C_mul Units.ne_zero IsDomain.toNontrivial
sub_mod 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instMod instSub DivisionRing.toRing Field.toDivisionRing	—	sub_modByMonic

Polynomial.IsRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_div_eq 📖	mathematical	Polynomial.IsRoot DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Polynomial Polynomial.instMul Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.instDiv	—	Polynomial.mul_div_eq_iff_isRoot

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normalize_eq_self 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe MonoidWithZeroHom Polynomial MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero CommSemiring.toCommMonoidWithZero Polynomial.commSemiring MonoidWithZeroHom.funLike normalize Polynomial.instNormalizationMonoid	—	Polynomial.coe_normUnit leadingCoeff normUnit_one RingHom.map_one mul_one

---

← Back to Index