Splits

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

Statistics

Metric	Count
Definitions Splits, rootOfSplits, rootOfSplits'	3
Theorems splits, C, C_mul, C_mul_X_pow, X, X_add_C, X_pow, X_sub_C, adjoin_rootSet_eq_range, aeval_eq_prod_aroots, aeval_eq_prod_aroots_of_monic, coeff_zero_eq_leadingCoeff_mul_prod_roots, coeff_zero_eq_prod_roots_of_monic, comp_X_add_C, comp_X_sub_C, comp_neg_X, comp_of_degree_le_one, comp_of_degree_le_one_of_invertible, comp_of_degree_le_one_of_monic, comp_of_map_degree_le_one, comp_of_natDegree_le_one, comp_of_natDegree_le_one_of_invertible, comp_of_natDegree_le_one_of_monic, def, degree_eq_card_roots, degree_eq_one_of_irreducible, degree_le_one_of_irreducible, dvd_iff_roots_le_roots, dvd_of_roots_le_roots, eq_X_sub_C_of_single_root, eq_prod_roots, eq_prod_roots_of_monic, eval_derivative, eval_derivative_div_eval_of_ne_zero, eval_derivative_eq_eval_mul_sum, eval_eq_prod_roots, eval_eq_prod_roots_of_monic, eval_root_derivative, exists_eval_eq_zero, image_rootSet, image_rootSet_of_map_ne_zero, listProd, map, map_roots, mem_lift_of_roots_mem_range, mem_range_of_isRoot, mem_subfield_of_isRoot, monomial, mul, multisetProd, natDegree_eq_card_roots, natDegree_eq_one_of_irreducible, natDegree_le_one_of_irreducible, neg, nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, nextCoeff_eq_neg_sum_roots_of_monic, of_algHom, of_degree_eq_one, of_degree_eq_two, of_degree_le_one, of_dvd, of_isScalarTower, of_natDegree_eq_one, of_natDegree_eq_two, of_natDegree_le_one, of_splits_map, of_splits_map_of_injective, one, pow, prod, roots_map, roots_map_of_injective, roots_map_of_ne_zero, roots_ne_zero, splits, splits_of_dvd, taylor, zero, adjoin_rootSet_eq_range, aeval_derivative_of_splits, aeval_eq_prod_aroots_sub_of_monic_of_splits, aeval_eq_prod_aroots_sub_of_splits, aeval_root_derivative_of_splits, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, coeff_zero_eq_prod_roots_of_monic_of_splits, degree_eq_card_roots, degree_eq_card_roots', degree_eq_one_of_irreducible_of_splits, eq_X_sub_C_of_splits_of_single_root, eq_prod_roots_of_monic_of_splits_id, eq_prod_roots_of_splits, eq_prod_roots_of_splits_id, eval_derivative_div_eval_of_ne_zero_of_splits, eval_derivative_eq_eval_mul_sum_of_splits, eval_derivative_of_splits, eval_eq_prod_roots_sub_of_monic_of_splits_id, eval_eq_prod_roots_sub_of_splits_id, eval_rootOfSplits, eval₂_derivative_of_splits, exists_root_of_splits, exists_root_of_splits', image_rootSet, map_rootOfSplits, map_rootOfSplits', map_sub_roots_sprod_eq_prod_map_eval, map_sub_sprod_roots_eq_prod_map_eval, mem_lift_of_splits_of_roots_mem_range, natDegree_eq_card_roots, natDegree_eq_card_roots', nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits, nextCoeff_eq_neg_sum_roots_of_monic_of_splits, prod_roots_eq_coeff_zero_of_monic_of_splits, rootOfSplits'_eq_rootOfSplits, roots_map, roots_ne_zero_of_splits, roots_ne_zero_of_splits', splits_C, splits_X, splits_X_pow, splits_X_sub_C, splits_X_sub_C_mul_iff, splits_comp_of_splits, splits_id_iff_splits, splits_id_of_splits, splits_iff, splits_iff_card_roots, splits_iff_comp_splits_of_degree_eq_one, splits_iff_comp_splits_of_natDegree_eq_one, splits_iff_exists_multiset, splits_iff_exists_multiset', splits_iff_splits, splits_map_iff, splits_mul, splits_mul_iff, splits_neg_iff, splits_of_algHom, splits_of_comp, splits_of_degree_eq_one, splits_of_degree_eq_two, splits_of_degree_le_one, splits_of_degree_le_one_of_invertible, splits_of_degree_le_one_of_monic, splits_of_degree_le_zero, splits_of_exists_multiset, splits_of_isScalarTower, splits_of_isUnit, splits_of_map_degree_eq_one, splits_of_map_eq_C, splits_of_natDegree_eq_one, splits_of_natDegree_eq_two, splits_of_natDegree_eq_zero, splits_of_natDegree_le_one, splits_of_natDegree_le_one_of_invertible, splits_of_natDegree_le_one_of_monic, splits_of_splits_gcd_left, splits_of_splits_gcd_right, splits_of_splits_id, splits_of_splits_mul, splits_of_splits_mul', splits_of_splits_of_dvd, splits_one, splits_pow, splits_prod, splits_prod_iff, splits_zero, sum_roots_eq_nextCoeff_of_monic_of_split	166
Total	169

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
splits 📖	mathematical	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Splits	—	Polynomial.splits_of_natDegree_eq_zero Polynomial.natDegree_eq_zero_of_isUnit

Polynomial

Definitions

Name	Category	Theorems
Splits 📖	MathDef	97 math math: splits_iff_exists_multiset, X_pow_sub_C_splits_of_isPrimitiveRoot, splits_of_map_eq_C, splits_of_natDegree_le_one, splits_neg_iff, Splits.monomial, Normal.splits', splits_of_degree_le_zero, IsSplittingField.splits_iff, Subfield.splits_bot, splits_map_iff, Gal.restrictDvd_def, X_pow_sub_one_splits, splits_zero, Cubic.splits_iff_card_roots, IsAlgClosed.splits_codomain, Normal.splits, Splits.X_pow, splits_iff_comp_splits_of_natDegree_eq_one, splits_of_natDegree_le_one_of_invertible, IsNormalClosure.splits, splits_C, splits_one, splits_iff_comp_splits_of_degree_eq_one, IsCyclotomicExtension.splits_cyclotomic, splits_of_natDegree_eq_zero, Splits.zero, Splits.X, IsAlgClosed.factors, IsCyclotomicExtension.splits_X_pow_sub_one, Splits.def, splits_iff, IsSplittingField.splits, IsSplittingField.splits', IsSepClosed.splits_domain, SplittingField.splits, splits_id_iff_splits, Matrix.IsHermitian.splits_charpoly, Cubic.splits_iff_roots_eq_three, Splits.X_add_C, FiniteField.splits_X_pow_nat_card_sub_X, ConjRootClass.splits_minpoly, splits_iff_card_roots, splits_mul_iff, AlgebraicClosure.Monics.splits_finsetProd, splits_of_natDegree_eq_two, splits_of_degree_le_one_of_invertible, Splits.of_natDegree_eq_one, Splits.C_mul_X_pow, PerfectField.splits_of_natSepDegree_eq_one, Algebra.IsAlgebraic.isNormalClosure_iff, Gal.splits_in_splittingField_of_comp, splits_of_splits_mul, normal_iff, Splits.of_degree_eq_two, FiniteField.splits_X_pow_card_sub_X, IsSepClosed.splits_codomain, Splits.X_sub_C, splits_of_degree_eq_one, splits_of_natDegree_eq_one, IntermediateField.isSplittingField_iff, splits_of_degree_le_one, Splits.of_natDegree_le_one, perfectField_iff_splits_of_natSepDegree_eq_one, SplittingFieldAux.splits, splits_X_sub_C_mul_iff, Splits.of_degree_le_one, splits_prod_iff, splits_of_degree_le_one_of_monic, Splits.of_degree_eq_one, IsUnit.splits, IsAlgClosed.splits, splits_X, Normal.out, splits_X_sub_C, IsSepClosed.factors_of_separable, cyclotomic'_splits, IsSepClosed.splits_of_separable, splits_iff_exists_multiset', splits_X_pow, splits_of_exists_multiset, Monic.exists_splits_map, splits_of_splits_mul', splits_iff_splits, IsSplittingField.IsScalarTower.splits, splits_of_map_degree_eq_one, Splits.C, Gal.splits_ℚ_ℂ, IsGalois.splits, IsAlgClosed.splits_domain, isSplittingField_iff_intermediateField, splits_of_degree_eq_two, Splits.of_natDegree_eq_two, splits_of_natDegree_le_one_of_monic, splits_of_isUnit, Splits.one, GaloisField.splits_zmod_X_pow_sub_X
rootOfSplits 📖	CompOp	4 math math: map_rootOfSplits, rootOfSplits'_eq_rootOfSplits, map_rootOfSplits', eval_rootOfSplits
rootOfSplits' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_rootSet_eq_range 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring map algebraMap	Algebra.adjoin rootSet AlgHom.range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Splits.adjoin_rootSet_eq_range
aeval_derivative_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff Multiset.sum Multiset.map Multiset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase roots	—	Splits.eval_derivative
aeval_eq_prod_aroots_sub_of_monic_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring map algebraMap Monic	DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing aroots	—	Splits.aeval_eq_prod_aroots_of_monic
aeval_eq_prod_aroots_sub_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring map algebraMap	DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom Semiring.toNonAssocSemiring RingHom.instFunLike leadingCoeff Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing aroots	—	Splits.aeval_eq_prod_aroots
aeval_root_derivative_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic Multiset Multiset.instMembership roots	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase	—	Splits.eval_root_derivative
coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne natDegree leadingCoeff Multiset.prod CommRing.toCommMonoid roots	—	Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots
coeff_zero_eq_prod_roots_of_monic_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne natDegree Multiset.prod CommRing.toCommMonoid roots	—	Splits.coeff_zero_eq_prod_roots_of_monic
degree_eq_card_roots 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	degree WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Multiset.card roots	—	Splits.degree_eq_card_roots
degree_eq_card_roots' 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	degree WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Multiset.card roots	—	Splits.degree_eq_card_roots
degree_eq_one_of_irreducible_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	degree WithBot WithBot.one Nat.instOne	—	Splits.degree_eq_one_of_irreducible
eq_X_sub_C_of_splits_of_single_root 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring roots Multiset Multiset.instSingleton	Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff instSub CommRing.toRing X	—	Splits.eq_X_sub_C_of_single_root
eq_prod_roots_of_monic_of_splits_id 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	Multiset.prod Polynomial CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C roots	—	Splits.eq_prod_roots_of_monic
eq_prod_roots_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X roots	—	Splits.eq_prod_roots
eq_prod_roots_of_splits_id 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X roots	—	Splits.eq_prod_roots
eval_derivative_div_eval_of_ne_zero_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Multiset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.map AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup roots instIsDomain	—	Splits.eval_derivative_div_eval_of_ne_zero
eval_derivative_eq_eval_mul_sum_of_splits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.sum Multiset.map DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup roots instIsDomain	—	Splits.eval_derivative_eq_eval_mul_sum
eval_derivative_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff Multiset.sum Multiset.map Multiset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase roots	—	Splits.eval_derivative
eval_eq_prod_roots_sub_of_monic_of_splits_id 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	eval Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing roots	—	Splits.eval_eq_prod_roots_of_monic
eval_eq_prod_roots_sub_of_splits_id 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing roots	—	Splits.eval_eq_prod_roots
eval_rootOfSplits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval rootOfSplits MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Splits.exists_eval_eq_zero
eval₂_derivative_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing leadingCoeff Multiset.sum Multiset.map Multiset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase roots	—	Splits.eval_derivative
exists_root_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Splits.exists_eval_eq_zero
exists_root_of_splits' 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Splits.exists_eval_eq_zero
image_rootSet 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring map algebraMap	Set.image DFunLike.coe AlgHom AlgHom.funLike rootSet	—	Splits.image_rootSet
map_rootOfSplits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval rootOfSplits MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eval_rootOfSplits
map_rootOfSplits' 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	eval rootOfSplits MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eval_rootOfSplits
map_sub_roots_sprod_eq_prod_map_eval 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring Splits	Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing SProd.sprod Multiset Multiset.instSProd roots Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Multiset.card eval	—	Multiset.map_swap_product Multiset.map_map Multiset.map_congr neg_mul one_mul neg_sub Multiset.prod_map_mul Multiset.map_const' Multiset.card_product Multiset.prod_replicate map_sub_sprod_roots_eq_prod_map_eval
map_sub_sprod_roots_eq_prod_map_eval 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring Splits	Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing SProd.sprod Multiset Multiset.instSProd roots eval	—	Splits.eq_prod_roots one_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Monic.leadingCoeff Multiset.map_congr eval_multiset_prod Multiset.prod_map_product_eq_prod_prod Multiset.map_map eval_sub eval_X eval_C
mem_lift_of_splits_of_roots_mem_range 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	Polynomial Subsemiring Semiring.toNonAssocSemiring semiring Subsemiring.instSetLike lifts Ring.toSemiring	—	Splits.mem_lift_of_roots_mem_range
natDegree_eq_card_roots 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	natDegree Multiset.card roots	—	Splits.natDegree_eq_card_roots
natDegree_eq_card_roots' 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	natDegree Multiset.card roots	—	Splits.natDegree_eq_card_roots
nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	nextCoeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing leadingCoeff Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid roots	—	Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff
nextCoeff_eq_neg_sum_roots_of_monic_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	nextCoeff NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing roots	—	Splits.nextCoeff_eq_neg_sum_roots_of_monic
prod_roots_eq_coeff_zero_of_monic_of_splits 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne natDegree Multiset.prod CommRing.toCommMonoid roots	—	coeff_zero_eq_prod_roots_of_monic_of_splits
rootOfSplits'_eq_rootOfSplits 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map	rootOfSplits EuclideanDomain.toCommRing Field.toEuclideanDomain WithBot degree Ring.toSemiring DivisionRing.toRing Field.toDivisionRing WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree_map DivisionRing.isSimpleRing EuclideanDomain.toNontrivial	—	—
roots_map 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring	roots map Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Splits.map_roots
roots_ne_zero_of_splits 📖	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring	—	—	Splits.roots_ne_zero
roots_ne_zero_of_splits' 📖	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring	—	—	Splits.roots_ne_zero
splits_C 📖	mathematical	—	Splits DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Splits.C
splits_X 📖	mathematical	—	Splits X	—	Splits.X
splits_X_pow 📖	mathematical	—	Splits Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	Splits.X_pow
splits_X_sub_C 📖	mathematical	—	Splits Ring.toSemiring Polynomial instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Splits.X_sub_C
splits_X_sub_C_mul_iff 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Splits.eq_prod_roots mul_left_cancel₀ instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero X_sub_C_ne_zero IsDomain.toNontrivial mul_left_comm Multiset.prod_cons Multiset.map_cons Multiset.singleton_add roots_X_sub_C roots_mul mul_ne_zero instNoZeroDivisors IsDomain.to_noZeroDivisors one_mul leadingCoeff_X_sub_C leadingCoeff_mul Splits.mul Splits.X_sub_C
splits_comp_of_splits 📖	mathematical	Splits	map	—	Splits.map
splits_id_iff_splits 📖	mathematical	—	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	map_id
splits_id_of_splits 📖	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring map Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	—	—	Splits.of_splits_map
splits_iff 📖	mathematical	—	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instZero degree WithBot WithBot.one Nat.instOne	—	splits_iff_splits
splits_iff_card_roots 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Multiset.card roots natDegree	—	Splits.natDegree_eq_card_roots splits_iff_exists_multiset C_leadingCoeff_mul_prod_multiset_X_sub_C
splits_iff_comp_splits_of_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot WithBot.one Nat.instOne	Splits comp	—	splits_iff_comp_splits_of_natDegree_eq_one natDegree_eq_of_degree_eq_some
splits_iff_comp_splits_of_natDegree_eq_one 📖	mathematical	natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Splits comp	—	Splits.comp_of_natDegree_le_one Eq.le exists_eq_X_add_C_of_natDegree_le_one Mathlib.Tactic.Contrapose.contrapose₃ map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul zero_add natDegree_C comp_assoc add_comp mul_comp C_comp X_comp mul_assoc C_mul mul_inv_cancel₀ C_1 one_mul sub_add_cancel comp_X natDegree_C_mul IsDomain.to_noZeroDivisors instIsDomain inv_eq_zero natDegree_X_sub_C EuclideanDomain.toNontrivial le_refl
splits_iff_exists_multiset 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X	—	splits_iff_exists_multiset' Multiset.map_map Multiset.map_congr map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_neg_eq_add
splits_iff_exists_multiset' 📖	mathematical	—	Splits CommSemiring.toSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommSemiring.toCommMonoid commSemiring Multiset.map instAdd X	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MonoidHom.coe_mrange Submonoid.mem_sup Submonoid.closure_eq Submonoid.closure_union Splits.eq_1 Submonoid.exists_multiset_of_mem_closure Multiset.map_map Multiset.map_congr Multiset.map_id' leadingCoeff_mul_monic monic_multiset_prod_of_monic leadingCoeff_C Zero.instNonempty Function.sometimes_spec Splits.mul Splits.C Splits.multisetProd
splits_iff_splits 📖	mathematical	—	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instZero degree WithBot WithBot.one Nat.instOne	—	Splits.degree_eq_one_of_irreducible Splits.of_dvd instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain UniqueFactorizationMonoid.factors_prod Splits.mul Splits.multisetProd Splits.of_degree_eq_one UniqueFactorizationMonoid.irreducible_of_factor UniqueFactorizationMonoid.dvd_of_mem_factors IsUnit.splits IsDomain.to_noZeroDivisors Units.isUnit
splits_map_iff 📖	mathematical	—	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield map CommSemiring.toSemiring CommRing.toCommSemiring RingHom.comp Semiring.toNonAssocSemiring	—	map_map
splits_mul 📖	mathematical	Splits	Polynomial instMul	—	Splits.mul
splits_mul_iff 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul	—	splits_of_natDegree_eq_zero natDegree_mul IsDomain.to_noZeroDivisors Splits.exists_eval_eq_zero degree_ne_of_natDegree_ne dvd_iff_isRoot instNoZeroDivisors add_comm natDegree_X_sub_C IsDomain.toNontrivial splits_X_sub_C_mul_iff mul_assoc Prime.dvd_mul prime_X_sub_C mul_comm Splits.mul
splits_neg_iff 📖	mathematical	—	Splits Ring.toSemiring Polynomial instNeg	—	Splits.neg neg_neg
splits_of_algHom 📖	—	Splits map CommSemiring.toSemiring algebraMap	—	—	Splits.of_algHom
splits_of_comp 📖	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring map Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	—	—	Splits.of_splits_map
splits_of_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring WithBot WithBot.one Nat.instOne	Splits	—	Splits.of_degree_eq_one
splits_of_degree_eq_two 📖	mathematical	degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Splits	—	Splits.of_degree_eq_two
splits_of_degree_le_one 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree DivisionSemiring.toSemiring WithBot.one Nat.instOne	Splits	—	Splits.of_degree_le_one
splits_of_degree_le_one_of_invertible 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree WithBot.one Nat.instOne	Splits	—	splits_of_natDegree_le_one_of_invertible natDegree_le_of_degree_le
splits_of_degree_le_one_of_monic 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree WithBot.one Nat.instOne Monic	Splits	—	splits_of_natDegree_le_one_of_monic natDegree_le_of_degree_le
splits_of_degree_le_zero 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	Splits	—	splits_of_natDegree_eq_zero natDegree_eq_zero_iff_degree_le_zero
splits_of_exists_multiset 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C leadingCoeff Multiset.prod CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X	—	splits_iff_exists_multiset
splits_of_isScalarTower 📖	—	Splits CommSemiring.toSemiring map algebraMap	—	—	Splits.of_isScalarTower
splits_of_isUnit 📖	mathematical	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	Splits	—	IsUnit.splits
splits_of_map_degree_eq_one 📖	mathematical	degree DivisionSemiring.toSemiring WithBot WithBot.one Nat.instOne	Splits	—	Splits.of_degree_eq_one
splits_of_map_eq_C 📖	mathematical	map CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	Splits	—	Splits.C
splits_of_natDegree_eq_one 📖	mathematical	natDegree DivisionSemiring.toSemiring	Splits	—	Splits.of_natDegree_eq_one
splits_of_natDegree_eq_two 📖	mathematical	natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Splits	—	Splits.of_natDegree_eq_two
splits_of_natDegree_eq_zero 📖	mathematical	natDegree	Splits	—	natDegree_eq_zero
splits_of_natDegree_le_one 📖	mathematical	natDegree DivisionSemiring.toSemiring	Splits	—	Splits.of_natDegree_le_one
splits_of_natDegree_le_one_of_invertible 📖	mathematical	natDegree	Splits	—	exists_eq_X_add_C_of_natDegree_le_one eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul zero_add natDegree_add_C natDegree_C_mul_X coeff_add coeff_mul_X coeff_C_zero coeff_C_succ add_zero mul_invOf_cancel_left C_mul mul_add Distrib.leftDistribClass Splits.mul Splits.C Splits.X_add_C
splits_of_natDegree_le_one_of_monic 📖	mathematical	natDegree Monic	Splits	—	splits_of_natDegree_le_one_of_invertible Monic.leadingCoeff
splits_of_splits_gcd_left 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq	—	Splits.of_dvd instIsDomain EuclideanDomain.gcd_dvd_left
splits_of_splits_gcd_right 📖	mathematical	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	EuclideanDomain.gcd Polynomial instEuclideanDomain instDecidableEq	—	Splits.of_dvd instIsDomain EuclideanDomain.gcd_dvd_right
splits_of_splits_id 📖	mathematical	Splits	map	—	Splits.map
splits_of_splits_mul 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul	—	splits_mul_iff
splits_of_splits_mul' 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial instMul	—	splits_mul_iff
splits_of_splits_of_dvd 📖	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing	—	—	Splits.of_dvd
splits_one 📖	mathematical	—	Splits Polynomial instOne	—	Splits.one
splits_pow 📖	mathematical	Splits	Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Splits.pow
splits_prod 📖	mathematical	Splits CommSemiring.toSemiring	Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring	—	Splits.prod
splits_prod_iff 📖	mathematical	—	Splits CommSemiring.toSemiring CommRing.toCommSemiring Finset.prod Polynomial CommRing.toCommMonoid commRing	—	Splits.of_dvd Finset.prod_ne_zero_iff nontrivial IsDomain.toNontrivial instNoZeroDivisors IsDomain.to_noZeroDivisors Finset.dvd_prod_of_mem Splits.prod
splits_zero 📖	mathematical	—	Splits Polynomial instZero	—	Splits.zero
sum_roots_eq_nextCoeff_of_monic_of_split 📖	mathematical	Splits CommSemiring.toSemiring CommRing.toCommSemiring Monic	nextCoeff NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing roots	—	nextCoeff_eq_neg_sum_roots_of_monic_of_splits

Polynomial.Splits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C 📖	mathematical	—	Polynomial.Splits DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Submonoid.mem_closure_of_mem Set.mem_union_left
C_mul 📖	mathematical	Polynomial.Splits	Polynomial Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	mul C
C_mul_X_pow 📖	mathematical	—	Polynomial.Splits Polynomial Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	C_mul X_pow
X 📖	mathematical	—	Polynomial.Splits Polynomial.X	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass add_zero X_add_C
X_add_C 📖	mathematical	—	Polynomial.Splits Polynomial Polynomial.instAdd Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Submonoid.mem_closure_of_mem Set.mem_union_right
X_pow 📖	mathematical	—	Polynomial.Splits Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	pow X
X_sub_C 📖	mathematical	—	Polynomial.Splits Ring.toSemiring Polynomial Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass X_add_C
adjoin_rootSet_eq_range 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap	Algebra.adjoin Polynomial.rootSet AlgHom.range Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	image_rootSet Algebra.adjoin_image Algebra.map_top Subalgebra.map_injective RingHom.injective IsDomain.toNontrivial
aeval_eq_prod_aroots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap	DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.leadingCoeff Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.aroots	—	eval_eq_prod_roots Polynomial.leadingCoeff_map IsDomain.toNontrivial
aeval_eq_prod_aroots_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap Polynomial.Monic	DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.aroots	—	eval_eq_prod_roots_of_monic Polynomial.Monic.map
coeff_zero_eq_leadingCoeff_mul_prod_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.natDegree Polynomial.leadingCoeff Multiset.prod CommRing.toCommMonoid Polynomial.roots	—	eq_prod_roots Polynomial.coeff_zero_eq_eval_zero Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_multiset_prod Multiset.map_map Multiset.map_congr Polynomial.eval_sub Polynomial.eval_X zero_sub Multiset.prod_map_neg natDegree_eq_card_roots mul_assoc mul_left_comm
coeff_zero_eq_prod_roots_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic	Polynomial.coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.natDegree Multiset.prod CommRing.toCommMonoid Polynomial.roots	—	coeff_zero_eq_leadingCoeff_mul_prod_roots Polynomial.Monic.leadingCoeff mul_one
comp_X_add_C 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring	Polynomial.comp Polynomial Polynomial.instAdd Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	comp_of_natDegree_le_one_of_monic Eq.trans_le Polynomial.natDegree_add_C Polynomial.natDegree_X_le Polynomial.monic_X_add_C
comp_X_sub_C 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.comp Polynomial Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	comp_of_natDegree_le_one_of_monic Eq.trans_le Polynomial.natDegree_sub_C Polynomial.natDegree_X_le Polynomial.monic_X_sub_C
comp_neg_X 📖	mathematical	Polynomial.Splits Ring.toSemiring	Polynomial.comp Polynomial Polynomial.instNeg Polynomial.X	—	Submonoid.closure_induction Polynomial.C_comp Polynomial.add_comp Polynomial.X_comp neg_add_eq_sub neg_sub neg X_sub_C Polynomial.one_comp mul Polynomial.mul_comp_neg_X
comp_of_degree_le_one 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne	Polynomial.comp	—	comp_of_natDegree_le_one Polynomial.natDegree_le_of_degree_le
comp_of_degree_le_one_of_invertible 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne	Polynomial.comp	—	comp_of_natDegree_le_one_of_invertible Polynomial.natDegree_le_of_degree_le
comp_of_degree_le_one_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne Polynomial.Monic	Polynomial.comp	—	comp_of_natDegree_le_one_of_monic Polynomial.natDegree_le_of_degree_le
comp_of_map_degree_le_one 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne	Polynomial.comp	—	comp_of_degree_le_one
comp_of_natDegree_le_one 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.natDegree	Polynomial.comp	—	eq_or_ne Polynomial.comp_zero comp_of_natDegree_le_one_of_invertible Polynomial.leadingCoeff_ne_zero
comp_of_natDegree_le_one_of_invertible 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring Polynomial.natDegree	Polynomial.comp	—	lt_or_eq_of_le Polynomial.eq_C_of_natDegree_eq_zero Polynomial.comp_C Polynomial.splits_iff_exists_multiset' Polynomial.mul_comp Polynomial.C_comp Polynomial.multiset_prod_comp mul C multisetProd Polynomial.splits_of_natDegree_le_one_of_invertible Polynomial.add_comp Polynomial.X_comp Polynomial.natDegree_add_C Polynomial.coeff_add Polynomial.coeff_C_succ add_zero Polynomial.leadingCoeff.eq_1
comp_of_natDegree_le_one_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring Polynomial.natDegree Polynomial.Monic	Polynomial.comp	—	comp_of_natDegree_le_one_of_invertible Polynomial.Monic.leadingCoeff
def 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial Polynomial.instZero Polynomial.degree WithBot WithBot.one Nat.instOne	—	Polynomial.splits_iff_splits
degree_eq_card_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.degree WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Multiset.card Polynomial.roots	—	Polynomial.degree_eq_iff_natDegree_eq natDegree_eq_card_roots
degree_eq_one_of_irreducible 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.degree WithBot WithBot.one Nat.instOne	—	le_antisymm degree_le_one_of_irreducible WithBot.one_le_iff_pos Nat.instZeroLEOneClass Polynomial.degree_pos_of_irreducible
degree_le_one_of_irreducible 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne	—	Polynomial.degree_le_of_natDegree_le natDegree_le_one_of_irreducible
dvd_iff_roots_le_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Polynomial.roots instIsDomain	—	instIsDomain Polynomial.roots.le_of_dvd dvd_of_roots_le_roots
dvd_of_roots_le_roots 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	—	instIsDomain eq_prod_roots Polynomial.C_mul_dvd Polynomial.leadingCoeff_ne_zero Dvd.dvd.trans Multiset.prod_dvd_prod_of_le Multiset.map_le_map Polynomial.prod_multiset_X_sub_C_dvd
eq_X_sub_C_of_single_root 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.roots Multiset Multiset.instSingleton	Polynomial Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.leadingCoeff Polynomial.instSub CommRing.toRing Polynomial.X	—	eq_prod_roots Multiset.prod_singleton Polynomial.leadingCoeff_mul IsDomain.to_noZeroDivisors Polynomial.leadingCoeff_C Polynomial.leadingCoeff_X_sub_C mul_one
eq_prod_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.leadingCoeff Multiset.prod CommRing.toCommMonoid Polynomial.commRing Multiset.map Polynomial.instSub CommRing.toRing Polynomial.X Polynomial.roots	—	Polynomial.leadingCoeff_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Multiset.map_congr Polynomial.roots.congr_simp Polynomial.roots_zero mul_one Polynomial.splits_iff_exists_multiset Polynomial.roots_C_mul Polynomial.roots_multiset_prod_X_sub_C
eq_prod_roots_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic	Multiset.prod Polynomial CommRing.toCommMonoid Polynomial.commRing Multiset.map Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.roots	—	eq_prod_roots Polynomial.Monic.leadingCoeff Polynomial.C_1 one_mul
eval_derivative 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.leadingCoeff Multiset.sum Multiset.map Multiset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase Polynomial.roots	—	eq_prod_roots Polynomial.derivative_mul Polynomial.derivative_C MulZeroClass.zero_mul Polynomial.derivative_prod Multiset.map_congr Polynomial.derivative_sub Polynomial.derivative_X sub_zero mul_one zero_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_multisetSum Multiset.map_map Polynomial.eval_multiset_prod Polynomial.eval_sub Polynomial.eval_X
eval_derivative_div_eval_of_ne_zero 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing Polynomial.eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Multiset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.map AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Polynomial.roots instIsDomain	—	instIsDomain eval_derivative_eq_eval_mul_sum mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass
eval_derivative_eq_eval_mul_sum 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Polynomial.eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.sum Multiset.map DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Polynomial.roots instIsDomain	—	instIsDomain eval_derivative eval_eq_prod_roots Multiset.map_congr mul_assoc Multiset.prod_map_erase mul_one_div mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass
eval_eq_prod_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.eval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.leadingCoeff Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.roots	—	eq_prod_roots Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_multiset_prod Multiset.map_map Multiset.map_congr Polynomial.eval_sub Polynomial.eval_X
eval_eq_prod_roots_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic	Polynomial.eval Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.roots	—	eval_eq_prod_roots Polynomial.Monic.leadingCoeff one_mul
eval_root_derivative 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic Multiset Multiset.instMembership Polynomial.roots	Polynomial.eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Multiset.erase	—	Polynomial.eval_multiset_prod_X_sub_C_derivative eq_prod_roots_of_monic
exists_eval_eq_zero 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.splits_iff_exists_multiset Polynomial.leadingCoeff_eq_zero Polynomial.eval_zero Zero.instNonempty Multiset.empty_or_exists_mem Polynomial.degree_C mul_one Multiset.prod_zero Multiset.map_zero Multiset.exists_cons_of_mem Multiset.map_cons Multiset.prod_cons Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_sub Polynomial.eval_X sub_self MulZeroClass.zero_mul MulZeroClass.mul_zero
image_rootSet 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap	Set.image DFunLike.coe AlgHom AlgHom.funLike Polynomial.rootSet	—	Polynomial.rootSet.eq_1 Finset.coe_image Multiset.toFinset_map AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.coe_toRingHom roots_map Polynomial.map_map AlgHom.comp_algebraMap
image_rootSet_of_map_ne_zero 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map algebraMap	Set.image DFunLike.coe AlgHom AlgHom.funLike Polynomial.rootSet	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.map_map AlgHom.comp_algebraMap roots_map_of_ne_zero Multiset.map_congr Multiset.toFinset_map Finset.coe_image
listProd 📖	mathematical	Polynomial.Splits	Polynomial Polynomial.instMul Polynomial.instOne	—	list_prod_mem Submonoid.instSubmonoidClass
map 📖	mathematical	Polynomial.Splits	Polynomial.map	—	Submonoid.closure_induction Polynomial.map_C Polynomial.map_add Polynomial.map_X Polynomial.map_one Polynomial.map_mul
map_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.roots Polynomial.map Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	roots_map
mem_lift_of_roots_mem_range 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	Polynomial Subsemiring Semiring.toNonAssocSemiring Polynomial.semiring Subsemiring.instSetLike Polynomial.lifts Ring.toSemiring	—	eq_prod_roots_of_monic Polynomial.lifts_iff_liftsRing Subring.multiset_prod_mem Multiset.mem_map Subring.sub_mem Polynomial.X_mem_lifts Polynomial.C'_mem_lifts
mem_range_of_isRoot 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.IsRoot Polynomial.map	Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	—	Multiset.mem_map roots_map Polynomial.mem_roots Polynomial.map_ne_zero IsDomain.toNontrivial
mem_subfield_of_isRoot 📖	—	Polynomial.Splits Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField Polynomial.IsRoot DivisionRing.toDivisionSemiring Polynomial.map Subfield.toDivisionRing Subfield.subtype	—	—	mem_range_of_isRoot instIsDomain DivisionRing.isSimpleRing
monomial 📖	mathematical	—	Polynomial.Splits DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial	—	—
mul 📖	mathematical	Polynomial.Splits	Polynomial Polynomial.instMul	—	MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass
multisetProd 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring	Multiset.prod Polynomial CommSemiring.toCommMonoid Polynomial.commSemiring	—	multiset_prod_mem Submonoid.instSubmonoidClass
natDegree_eq_card_roots 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.natDegree Multiset.card Polynomial.roots	—	Polynomial.leadingCoeff_eq_zero Polynomial.roots.congr_simp Polynomial.roots_zero eq_prod_roots Polynomial.natDegree_C_mul IsDomain.to_noZeroDivisors Polynomial.natDegree_multiset_prod_X_sub_C_eq_card IsDomain.toNontrivial
natDegree_eq_one_of_irreducible 📖	mathematical	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.natDegree	—	Polynomial.natDegree_eq_of_degree_eq_some degree_eq_one_of_irreducible
natDegree_le_one_of_irreducible 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.natDegree	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.natDegree_of_subsingleton Nat.instCanonicallyOrderedAdd Polynomial.splits_iff_exists_multiset' Multiset.empty_or_exists_mem mul_one Polynomial.natDegree_C Multiset.exists_cons_of_mem instIsDedekindFiniteMonoid Multiset.prod_cons Multiset.map_cons le_imp_le_of_le_of_le Polynomial.natDegree_mul_le le_refl Polynomial.natDegree_add_C Polynomial.natDegree_X zero_add
neg 📖	mathematical	Polynomial.Splits Ring.toSemiring	Polynomial Polynomial.instNeg	—	neg_one_mul Polynomial.C_1 Polynomial.C_neg C_mul
nextCoeff_eq_neg_sum_roots_mul_leadingCoeff 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.nextCoeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Polynomial.leadingCoeff Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Polynomial.roots	—	eq_prod_roots Polynomial.nextCoeff_C_mul IsDomain.to_noZeroDivisors Polynomial.Monic.nextCoeff_multiset_prod Multiset.map_congr Polynomial.nextCoeff_X_sub_C Multiset.sum_map_neg' mul_neg neg_mul
nextCoeff_eq_neg_sum_roots_of_monic 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.Monic	Polynomial.nextCoeff NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.roots	—	nextCoeff_eq_neg_sum_roots_mul_leadingCoeff Polynomial.Monic.leadingCoeff neg_mul one_mul
of_algHom 📖	—	Polynomial.Splits Polynomial.map CommSemiring.toSemiring algebraMap	—	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap Polynomial.map_map map
of_degree_eq_one 📖	mathematical	Polynomial.degree DivisionSemiring.toSemiring WithBot WithBot.one Nat.instOne	Polynomial.Splits	—	of_degree_le_one Eq.le
of_degree_eq_two 📖	mathematical	Polynomial.degree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Polynomial.Splits	—	Nat.instAtLeastTwoHAddOfNat of_natDegree_eq_two Polynomial.natDegree_eq_of_degree_eq_some
of_degree_le_one 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree DivisionSemiring.toSemiring WithBot.one Nat.instOne	Polynomial.Splits	—	of_natDegree_le_one Polynomial.natDegree_le_of_degree_le
of_dvd 📖	—	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	—	—	Polynomial.splits_mul_iff Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors
of_isScalarTower 📖	—	Polynomial.Splits CommSemiring.toSemiring Polynomial.map algebraMap	—	—	of_algHom
of_natDegree_eq_one 📖	mathematical	Polynomial.natDegree DivisionSemiring.toSemiring	Polynomial.Splits	—	of_natDegree_le_one Eq.le
of_natDegree_eq_two 📖	mathematical	Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Polynomial.Splits	—	Polynomial.natDegree_divByMonic Polynomial.monic_X_sub_C Polynomial.natDegree_X_sub_C EuclideanDomain.toNontrivial Polynomial.mul_divByMonic_eq_iff_isRoot Polynomial.splits_mul_iff instIsDomain Polynomial.X_sub_C_ne_zero X_sub_C of_natDegree_eq_one
of_natDegree_le_one 📖	mathematical	Polynomial.natDegree DivisionSemiring.toSemiring	Polynomial.Splits	—	Polynomial.exists_eq_X_add_C_of_natDegree_le_one map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul zero_add mul_inv_cancel_left₀ Polynomial.C_mul mul_add Distrib.leftDistribClass C_mul X_add_C
of_splits_map 📖	—	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	—	—	of_splits_map_of_injective RingHom.injective IsDomain.toNontrivial
of_splits_map_of_injective 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Polynomial.Splits Polynomial.map Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range	—	—	Polynomial.splits_iff_exists_multiset Polynomial.map_injective eq_prod_roots Polynomial.leadingCoeff_map_of_injective Multiset.map_pmap Polynomial.map_mul Polynomial.map_C Polynomial.map_multiset_prod Multiset.pmap.congr_simp Polynomial.map_sub Polynomial.map_X Multiset.pmap_eq_map
one 📖	mathematical	—	Polynomial.Splits Polynomial Polynomial.instOne	—	C
pow 📖	mathematical	Polynomial.Splits	Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	pow_mem Submonoid.instSubmonoidClass
prod 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring	Finset.prod Polynomial CommSemiring.toCommMonoid Polynomial.commSemiring	—	prod_mem Submonoid.instSubmonoidClass
roots_map 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.roots Polynomial.map Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	roots_map_of_injective RingHom.injective IsDomain.toNontrivial
roots_map_of_injective 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	Polynomial.roots Polynomial.map Multiset.map	—	Polynomial.roots_map_of_injective_of_card_eq_natDegree natDegree_eq_card_roots
roots_map_of_ne_zero 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.roots Polynomial.map Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Submonoid.closure_induction Polynomial.roots.congr_simp Polynomial.map_C Polynomial.roots_C Multiset.map_congr Polynomial.map_add Polynomial.map_X Polynomial.roots_X_add_C map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.map_one Polynomial.roots_one Polynomial.map_mul Polynomial.roots_mul Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.map_zero Multiset.map_add
roots_ne_zero 📖	—	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	—	—	natDegree_eq_card_roots
splits 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial Polynomial.instZero WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.one Nat.instOne	—	Polynomial.degree_le_of_natDegree_le natDegree_le_one_of_irreducible of_dvd
splits_of_dvd 📖	—	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	—	—	of_dvd
taylor 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.taylor	—	add_assoc map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass X_add_C Submonoid.closure_induction Polynomial.taylor_C SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Polynomial.taylor_X Polynomial.taylor_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.taylor_mul
zero 📖	mathematical	—	Polynomial.Splits Polynomial Polynomial.instZero	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass C

---

← Back to Index