Monic

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

Statistics

Metric	Count
Definitions Monic, Monic, Monic, MonicDegreeEq, map, mk	6
Theorems monic_map_iff, add_of_left, add_of_right, as_sum, comp, comp_X_add_C, comp_X_sub_C, degree_le_zero_iff_eq_one, degree_map, degree_mul_comm, eq_one_of_isUnit, eq_one_of_map_eq_one, irreducible_iff_lt_natDegree_lt, irreducible_iff_natDegree, irreducible_iff_natDegree', isRegular, isUnit_iff, map, mul, mul_left_eq_zero_iff, mul_left_ne_zero, mul_natDegree_lt_iff, mul_right_eq_zero_iff, mul_right_ne_zero, natDegree_eq_zero_iff_eq_one, natDegree_map, natDegree_mul, natDegree_mul', natDegree_mul_comm, natDegree_pow, nextCoeff_mul, nextCoeff_multiset_prod, nextCoeff_pow, nextCoeff_prod, not_dvd_of_degree_lt, not_dvd_of_natDegree_lt, not_irreducible_iff_exists_add_mul_eq_coeff, of_mul_monic_left, of_mul_monic_right, pow, sub_of_left, sub_of_right, coeff_of_ge, degree, map_coe, mk_coe, monic, natDegree, degree_smul_of_smul_regular, eq_of_monic_of_associated, irreducible_of_monic, isUnit_leadingCoeff_mul_left_eq_zero_iff, isUnit_leadingCoeff_mul_right_eq_zero_iff, leadingCoeff_map', leadingCoeff_of_injective, leadingCoeff_smul_of_smul_regular, monic_C_mul_of_mul_leadingCoeff_eq_one, monic_X_add_C, monic_X_pow_add, monic_X_pow_add_C, monic_X_pow_sub, monic_X_pow_sub_C, monic_X_sub_C, monic_finprod_of_monic, monic_mul_C_of_leadingCoeff_mul_eq_one, monic_multiset_prod_of_monic, monic_of_injective, monic_of_isUnit_leadingCoeff_inv_smul, monic_prod_of_monic, monic_zero_iff_subsingleton, monic_zero_iff_subsingleton', natDegree_pow_X_add_C, natDegree_smul_of_smul_regular, not_isUnit_X_add_C, not_isUnit_X_pow_sub_one, not_monic_zero, not_monic_zero_iff	77
Total	83

AddMonoidAlgebra

Definitions

Name	Category	Theorems
Monic 📖	MathDef	4 math math: Monic.pow, Monic.mul, MvPolynomial.monic_esymm, monic_one

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monic_map_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	Polynomial.Monic Polynomial.map	—	Polynomial.Monic.map Polynomial.monic_of_injective

MonomialOrder

Definitions

Name	Category	Theorems
Monic 📖	MathDef	14 math math: monic_X_sub_C, monic_leadingTerm, Monic.of_subsingleton, monic_X_add_C, Monic.pow, monic_of_subsingleton, monic_monomial, monic_monomial_one, monic_C_one, Monic.mul, Monic.add_of_lt, monic_one, Monic.prod, monic_X

Polynomial

Definitions

Name	Category	Theorems
Monic 📖	MathDef	116 math math: monic_of_subsingleton, MonicDegreeEq.monic, monic_X_pow, LinearMap.exists_monic_and_aeval_eq_zero, monic_X_sub_C, FixedPoints.minpoly.monic, PowerBasis.minpolyGen_monic, Monic.add_of_left, lifts_and_degree_eq_and_monic, WeierstrassCurve.Affine.monic_polynomial, monic_toSubring, FirstOrder.Field.realize_genericMonicPolyHasRoot, minpoly.monic, monic_X_pow_add_C, monic_multisetProd_X_sub_C, monic_restriction, monic_map_iff, IsDistinguishedAt.monic, Monic.of_mul_monic_right, monic_X_pow_add, exists_monic_irreducible_factor, Cubic.monic_of_c_eq_one, Monic.geom_sum', monic_finprod_X_sub_C, monic_of_isUnit_leadingCoeff_inv_smul, int_coeff_of_cyclotomic', Monic.comp_X_sub_C, FirstOrder.Field.lift_genericMonicPoly, monic_of_monic_mapAlg, Monic.of_mul_monic_left, monic_multiset_prod_of_monic, monic_mapAlg_iff, monic_X_pow_sub_C, cyclotomic'.monic, not_monic_zero, ConjRootClass.monic_minpoly, Matrix.charpoly.univ_monic, exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, int_cyclotomic_rw, monic_X_add_C, LinearMap.charpoly_monic, monic_of_natDegree_le_of_coeff_eq_one, trinomial_monic, monic_C_mul_of_mul_leadingCoeff_eq_one, monic_integralNormalization, Irreducible.exists_dvd_monic_irreducible_of_isIntegral, monic_of_degree_le_of_coeff_eq_one, StandardEtalePair.monic_f, Function.Injective.monic_map_iff, prodXSubSMul.monic, monic_ascPochhammer, AlgebraicClosure.Monics.splits_finsetProd, Monic.comp, Cubic.monic_of_a_eq_one', isMonicOfDegree_iff', monic_prod_of_monic, Cubic.monic_of_b_eq_one', Cubic.monic_of_c_eq_one', AlgebraicClosure.toSplittingField_coeff, monic_expand_iff, monic_geom_sum_X, int_monic_iff, LinearRecurrence.charPoly_monic, monic_of_degree_le, monic_descPochhammer, Monic.sub_of_left, cyclotomic.monic, normalize_eq_self_iff_monic, AlgebraicClosure.Monics.map_eq_prod, Monic.sub_of_right, Monic.add_of_right, Monic.geom_sum, Cubic.monic_of_a_eq_one, monic_freeMonic, Monic.comp_X_add_C, monic_mul_C_of_leadingCoeff_mul_eq_one, monic_mul_leadingCoeff_inv, exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, Monic.pow, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, MulSemiringAction.monic_charpoly, LinearMap.polyCharpoly_monic, mem_normalizedFactors_iff, IsMonicOfDegree.monic, exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt, Monic.def, not_monic_zero_iff, monic_one, Cubic.monic_of_d_eq_one', Matrix.charpoly_monic, Monic.expand, Lagrange.nodal_monic, Cubic.monic_of_d_eq_one, monic_zero_iff_subsingleton', lifts_and_natDegree_eq_and_monic, monic_of_injective, Monic.map, Monic.mul, monic_annIdealGenerator, Cubic.monic_of_b_eq_one, monic_zero_iff_subsingleton, monic_normalize, monic_prod_X_sub_C, minpolyDiv_monic, exists_monic_aeval_eq_zero_forall_mem_of_mem_map, monic_scaleRoots_iff, monic_X, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, IsAdjoinRootMonic.monic, monic_finprod_of_monic, hermite_monic, Monic.neg_one_pow_natDegree_mul_comp_neg_X, RatFunc.monic_denom, monic_X_pow_sub, int_cyclotomic_spec
MonicDegreeEq 📖	CompOp	8 math math: UniversalCoprimeFactorizationRing.homEquiv_comp_snd, MvPolynomial.coe_mapEquivMonic_comp', UniversalCoprimeFactorizationRing.homEquiv_comp_fst, MvPolynomial.mapEquivMonic_symm_map_algebraMap, MvPolynomial.mapEquivMonic_symm_map, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.coe_mapEquivMonic_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_smul_of_smul_regular 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	degree Polynomial SMulZeroClass.toSMul instZero smulZeroClass	—	le_antisymm degree_le_iff_coeff_zero coeff_smul degree_lt_iff_coeff_zero le_rfl smul_zero
eq_of_monic_of_associated 📖	—	Monic Associated Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	—	Monic.eq_one_of_isUnit Monic.of_mul_monic_left Units.isUnit mul_one
irreducible_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instOne	—	Monic.eq_one_of_isUnit Irreducible.isUnit_or_isUnit IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid Monic.eq_1 leadingCoeff_mul leadingCoeff_C mul_comm mul_mul_mul_comm C_mul Monic.leadingCoeff C_1 mul_one
isUnit_leadingCoeff_mul_left_eq_zero_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	Polynomial instMul instZero	—	Monic.mul_left_eq_zero_iff monic_mul_C_of_leadingCoeff_mul_eq_one IsUnit.mul_val_inv mul_assoc MulZeroClass.zero_mul
isUnit_leadingCoeff_mul_right_eq_zero_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	Polynomial instMul instZero	—	ext coeff_smul coeff_mul Finset.mul_sum Finset.sum_congr mul_assoc Monic.mul_right_eq_zero_iff monic_of_isUnit_leadingCoeff_inv_smul smul_eq_zero_iff_eq MulZeroClass.mul_zero
leadingCoeff_map' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	leadingCoeff map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	leadingCoeff_map_of_injective
leadingCoeff_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	leadingCoeff map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	leadingCoeff_map_of_injective
leadingCoeff_smul_of_smul_regular 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	leadingCoeff Polynomial SMulZeroClass.toSMul instZero smulZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	leadingCoeff.eq_1 coeff_smul natDegree_smul_of_smul_regular
monic_C_mul_of_mul_leadingCoeff_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring leadingCoeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Monic Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Monic.leadingCoeff leadingCoeff_mul' leadingCoeff_C NeZero.one
monic_X_add_C 📖	mathematical	—	Monic Polynomial instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	monic_X_pow_add_C one_ne_zero pow_one
monic_X_pow_add 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree WithBot.natCast	Monic Polynomial instAdd Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	monic_of_degree_le le_trans degree_add_le max_le degree_X_pow_le le_of_lt coeff_add coeff_X_pow coeff_eq_zero_of_degree_lt add_zero
monic_X_pow_add_C 📖	mathematical	—	Monic Polynomial instAdd Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	monic_X_pow_add lt_of_le_of_lt degree_C_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial WithBot.instIsOrderedRing IsStrictOrderedRing.toIsOrderedRing WithBot.nontrivial
monic_X_pow_sub 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree Ring.toSemiring WithBot.natCast	Monic Ring.toSemiring Polynomial instSub Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X	—	sub_eq_add_neg monic_X_pow_add degree_neg
monic_X_pow_sub_C 📖	mathematical	—	Monic Ring.toSemiring Polynomial instSub Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass monic_X_pow_add_C
monic_X_sub_C 📖	mathematical	—	Monic Ring.toSemiring Polynomial instSub X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	sub_eq_add_neg C_neg monic_X_add_C
monic_finprod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	Monic CommSemiring.toSemiring finprod Polynomial CommSemiring.toCommMonoid commSemiring	—	finprod_def monic_prod_of_monic Set.Finite.mem_toFinset monic_one
monic_mul_C_of_leadingCoeff_mul_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring leadingCoeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Monic Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Monic.leadingCoeff leadingCoeff_mul' leadingCoeff_C NeZero.one
monic_multiset_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	Monic CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.map	—	Multiset.induction_on instIsEmptyFalse Multiset.map_cons Multiset.prod_cons Monic.mul Multiset.mem_cons_self Multiset.mem_cons_of_mem
monic_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Monic map	Monic	—	leadingCoeff_map_of_injective Monic.leadingCoeff RingHom.map_one
monic_of_isUnit_leadingCoeff_inv_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	Monic Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial Units.instSMul SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring Units.instInv IsUnit.unit leadingCoeff	—	Monic.def leadingCoeff_smul_of_smul_regular isSMulRegular_of_group Units.smul_def IsUnit.val_inv_mul
monic_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	Monic CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring	—	monic_multiset_prod_of_monic
monic_zero_iff_subsingleton 📖	mathematical	—	Monic Polynomial instZero	—	subsingleton_iff_zero_eq_one
monic_zero_iff_subsingleton' 📖	mathematical	—	Monic Polynomial instZero	—	monic_zero_iff_subsingleton Unique.instSubsingleton subsingleton_iff
natDegree_pow_X_add_C 📖	mathematical	—	natDegree Polynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	Monic.natDegree_pow monic_X_add_C natDegree_X_add_C mul_one
natDegree_smul_of_smul_regular 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	natDegree Polynomial SMulZeroClass.toSMul instZero smulZeroClass	—	smul_zero WithBot.charZero Nat.instCharZero degree_eq_natDegree Mathlib.Tactic.Contrapose.contrapose₄ IsSMulRegular.polynomial degree_smul_of_smul_regular
not_isUnit_X_add_C 📖	mathematical	—	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	Monic.natDegree_mul' monic_X_add_C right_ne_zero_of_mul_eq_one nontrivial natDegree_X_add_C natDegree_one
not_isUnit_X_pow_sub_one 📖	mathematical	—	IsUnit Polynomial Ring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub Monoid.toPow X instOne	—	eq_or_ne pow_zero sub_self NeZero.one nontrivial natDegree_one Monic.eq_one_of_isUnit monic_X_pow_sub_C natDegree_X_pow_sub_C
not_monic_zero 📖	mathematical	—	Monic Polynomial instZero	—	not_monic_zero_iff zero_ne_one NeZero.one
not_monic_zero_iff 📖	mathematical	—	Monic Polynomial instZero	—	Iff.not monic_zero_iff_subsingleton subsingleton_iff_zero_eq_one

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_of_left 📖	mathematical	Polynomial.Monic WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	Polynomial.Monic Polynomial Polynomial.instAdd	—	eq_1 add_comm Polynomial.leadingCoeff_add_of_degree_lt
add_of_right 📖	mathematical	Polynomial.Monic WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	Polynomial.Monic Polynomial Polynomial.instAdd	—	eq_1 Polynomial.leadingCoeff_add_of_degree_lt
as_sum 📖	mathematical	Polynomial.Monic	Polynomial Polynomial.instAdd Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.natDegree Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.range Polynomial.instMul DFunLike.coe RingHom RingHom.instFunLike Polynomial.C Polynomial.coeff	—	Polynomial.as_sum_range_C_mul_X_pow Finset.sum_range_succ_comm one_mul
comp 📖	mathematical	Polynomial.Monic	Polynomial.Monic Polynomial.comp	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.natDegree_comp_eq_of_mul_ne_zero leadingCoeff one_pow mul_one NeZero.one def Polynomial.leadingCoeff.eq_1 Polynomial.coeff_comp_degree_mul_degree
comp_X_add_C 📖	mathematical	Polynomial.Monic	Polynomial.Monic Polynomial.comp Polynomial Polynomial.instAdd Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim comp Polynomial.monic_X_add_C one_ne_zero Polynomial.natDegree_X_add_C
comp_X_sub_C 📖	mathematical	Polynomial.Monic Ring.toSemiring	Polynomial.Monic Ring.toSemiring Polynomial.comp Polynomial Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass comp_X_add_C
degree_le_zero_iff_eq_one 📖	mathematical	Polynomial.Monic	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Polynomial Polynomial.instOne	—	natDegree_eq_zero Polynomial.natDegree_eq_zero_iff_degree_le_zero
degree_map 📖	mathematical	Polynomial.Monic	Polynomial.degree Polynomial.map	—	leadingCoeff map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass NeZero.one
degree_mul_comm 📖	mathematical	Polynomial.Monic	Polynomial.degree Polynomial Polynomial.instMul	—	MulZeroClass.mul_zero MulZeroClass.zero_mul Polynomial.degree_mul' leadingCoeff one_mul Polynomial.leadingCoeff_ne_zero degree_mul add_comm
eq_one_of_isUnit 📖	mathematical	Polynomial.Monic IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial Polynomial.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton IsUnit.exists_right_inv natDegree_mul' right_ne_zero_of_mul_eq_one Polynomial.nontrivial natDegree_eq_zero add_eq_zero Polynomial.natDegree_one
eq_one_of_map_eq_one 📖	mathematical	Polynomial.Monic Polynomial.map Polynomial Polynomial.instOne	Polynomial Polynomial.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Polynomial.degree_map_eq_of_leadingCoeff_ne_zero leadingCoeff RingHom.map_one one_ne_zero NeZero.one Polynomial.degree_one WithBot.coe_eq_coe Polynomial.degree_eq_natDegree ne_zero Polynomial.leadingCoeff.eq_1 Polynomial.eq_C_of_degree_eq_zero
irreducible_iff_lt_natDegree_lt 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring	—	irreducible_iff_natDegree' of_mul_monic_left mul_comm dvd_mul_left
irreducible_iff_natDegree 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.natDegree	—	Polynomial.irreducible_of_monic natDegree_eq_zero
irreducible_iff_natDegree' 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Finset SetLike.instMembership Finset.instSetLike Finset.Ioc Nat.instPreorder Nat.instLocallyFiniteOrder Polynomial.natDegree	—	irreducible_iff_natDegree Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_two natDegree_mul add_le_add_iff_right covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le LT.lt.ne' LT.lt.trans_le Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq le_total mul_comm add_le_add_right add_le_add_left Nat.instCanonicallyOrderedAdd
isRegular 📖	mathematical	Polynomial.Monic Ring.toSemiring	IsRegular Polynomial Ring.toSemiring Polynomial.instMul	—	sub_eq_zero mul_right_eq_zero_iff mul_sub sub_self mul_left_eq_zero_iff sub_mul
isUnit_iff 📖	mathematical	Polynomial.Monic	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instOne	—	eq_one_of_isUnit isUnit_one
map 📖	mathematical	Polynomial.Monic	Polynomial.Monic Polynomial.map	—	subsingleton_or_nontrivial Polynomial.leadingCoeff_map_eq_of_isUnit_leadingCoeff RingHom.map_one isUnit_one
mul 📖	mathematical	Polynomial.Monic	Polynomial.Monic Polynomial Polynomial.instMul	—	subsingleton_of_zero_eq_one def mul_one Polynomial.leadingCoeff_mul' one_mul
mul_left_eq_zero_iff 📖	mathematical	Polynomial.Monic	Polynomial Polynomial.instMul Polynomial.instZero	—	MulZeroClass.zero_mul mul_left_ne_zero
mul_left_ne_zero 📖	—	Polynomial.Monic	—	—	mul_one Polynomial.degree_eq_bot degree_mul WithBot.add_eq_bot LT.lt.ne' lt_trans not_le degree_le_zero_iff_eq_one
mul_natDegree_lt_iff 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Polynomial.instMul Polynomial.instZero	—	LT.lt.ne' lt_of_le_of_ne MulZeroClass.mul_zero natDegree_eq_zero natDegree_mul' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
mul_right_eq_zero_iff 📖	mathematical	Polynomial.Monic	Polynomial Polynomial.instMul Polynomial.instZero	—	MulZeroClass.mul_zero mul_right_ne_zero
mul_right_ne_zero 📖	—	Polynomial.Monic	—	—	one_mul Polynomial.degree_eq_bot degree_mul_comm degree_mul WithBot.add_eq_bot LT.lt.ne' lt_trans not_le degree_le_zero_iff_eq_one
natDegree_eq_zero_iff_eq_one 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Polynomial.instOne	—	natDegree_eq_zero
natDegree_map 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial.map	—	le_antisymm Polynomial.natDegree_map_le Polynomial.le_natDegree_of_ne_zero Polynomial.coeff_map coeff_natDegree map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_ne_zero NeZero.one
natDegree_mul 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Polynomial.instMul	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.natDegree_of_subsingleton add_zero Polynomial.natDegree_mul' leadingCoeff mul_one NeZero.one
natDegree_mul' 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Polynomial.instMul	—	Polynomial.natDegree_mul' leadingCoeff one_mul
natDegree_mul_comm 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Polynomial.instMul	—	MulZeroClass.mul_zero MulZeroClass.zero_mul natDegree_mul' Polynomial.natDegree_mul' leadingCoeff mul_one add_comm
natDegree_pow 📖	mathematical	Polynomial.Monic	Polynomial.natDegree Polynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	pow_zero Polynomial.natDegree_one MulZeroClass.zero_mul pow_succ natDegree_mul pow add_comm
nextCoeff_mul 📖	mathematical	Polynomial.Monic	Polynomial.nextCoeff Polynomial Polynomial.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.reverse_mul leadingCoeff mul_one NeZero.one Polynomial.mul_coeff_one Polynomial.coeff_zero_reverse Polynomial.coeff_one_reverse one_mul add_comm
nextCoeff_multiset_prod 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Polynomial.nextCoeff CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid Polynomial.commSemiring Multiset.map Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Multiset.induction_on Polynomial.C_1 Polynomial.nextCoeff_C_eq_zero Multiset.map_cons Multiset.prod_cons Multiset.sum_cons nextCoeff_mul Multiset.mem_cons_self Polynomial.monic_multiset_prod_of_monic Multiset.mem_cons_of_mem
nextCoeff_pow 📖	mathematical	Polynomial.Monic	Polynomial.nextCoeff Polynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	pow_zero zero_smul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.nextCoeff_C_eq_zero pow_succ nextCoeff_mul pow succ_nsmul
nextCoeff_prod 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Polynomial.nextCoeff CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid Polynomial.commSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	nextCoeff_multiset_prod
not_dvd_of_degree_lt 📖	mathematical	Polynomial.Monic WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Polynomial.semiring	—	not_dvd_of_natDegree_lt Polynomial.natDegree_lt_natDegree
not_dvd_of_natDegree_lt 📖	mathematical	Polynomial.Monic Polynomial.natDegree	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring Polynomial.semiring	—	LT.lt.not_ge natDegree_mul' right_ne_zero_of_mul
not_irreducible_iff_exists_add_mul_eq_coeff 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring Polynomial.natDegree	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd	—	subsingleton_or_nontrivial Polynomial.natDegree_of_subsingleton Nat.instCharZero Nat.instAtLeastTwoHAddOfNat irreducible_iff_natDegree' Polynomial.natDegree_one Mathlib.Tactic.Push.not_forall_eq Polynomial.mul_coeff_zero add_right_cancel instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.Ioc_succ_singleton zero_add natDegree_mul nextCoeff_mul Polynomial.monic_X_add_C Polynomial.as_sum_range_C_mul_X_pow Finset.sum_range_succ Finset.sum_range_one coeff_natDegree Polynomial.C_mul Polynomial.C_add Polynomial.C_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Nat.cast_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd Polynomial.natDegree_add_C Polynomial.natDegree_X
of_mul_monic_left 📖	mathematical	Polynomial.Monic Polynomial Polynomial.instMul	Polynomial.Monic	—	Mathlib.Tactic.Contrapose.contrapose₁ def Polynomial.leadingCoeff_monic_mul
of_mul_monic_right 📖	mathematical	Polynomial.Monic Polynomial Polynomial.instMul	Polynomial.Monic	—	Mathlib.Tactic.Contrapose.contrapose₁ def Polynomial.leadingCoeff_mul_monic
pow 📖	mathematical	Polynomial.Monic	Polynomial.Monic Polynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	Polynomial.monic_one pow_succ mul
sub_of_left 📖	mathematical	Polynomial.Monic Ring.toSemiring WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	Polynomial.Monic Ring.toSemiring Polynomial Polynomial.instSub	—	sub_eq_add_neg add_of_left Polynomial.degree_neg
sub_of_right 📖	mathematical	Polynomial.leadingCoeff Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	Polynomial.Monic Ring.toSemiring Polynomial Polynomial.instSub	—	Polynomial.natDegree_neg Polynomial.coeff_neg neg_neg sub_eq_add_neg add_of_right Polynomial.degree_neg

Polynomial.MonicDegreeEq

Definitions

Name	Category	Theorems
map 📖	CompOp	8 math math: Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, MvPolynomial.coe_mapEquivMonic_comp', Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, map_coe, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, MvPolynomial.mapEquivMonic_symm_map_algebraMap, MvPolynomial.mapEquivMonic_symm_map
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_of_ge 📖	mathematical	—	Polynomial.coeff Polynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	LE.le.lt_of_ne
degree 📖	mathematical	—	Polynomial.degree Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring WithBot WithBot.natCast	—	Polynomial.degree_eq_of_le_of_coeff_ne_zero Polynomial.degree_le_of_natDegree_le Eq.le natDegree NeZero.one
map_coe 📖	mathematical	—	Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring map Polynomial.map	—	—
mk_coe 📖	mathematical	Polynomial.Monic Polynomial.natDegree	Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—
monic 📖	mathematical	—	Polynomial.Monic Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.Monic.eq_1 Polynomial.leadingCoeff.eq_1 natDegree
natDegree 📖	mathematical	—	Polynomial.natDegree Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Polynomial.natDegree_eq_of_le_of_coeff_ne_zero Polynomial.natDegree_le_iff_coeff_eq_zero NeZero.one

---

← Back to Index