RingDivision

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

Statistics

Metric	Count
Definitions `modByMonicHom`	1
Theorems `aeval_ne_zero_of_natDegree_ne_one`, `irreducible_of_degree_eq_one`, `mem_nonZeroDivisors`, `neg_one_pow_natDegree_mul_comp_neg_X`, `prime_of_degree_eq_one`, `aeval_modByMonic_eq_self_of_root`, `aeval_ne_zero_of_isCoprime`, `degree_eq_degree_of_associated`, `degree_pos_of_aeval_root`, `exists_multiset_roots`, `irreducible_C_mul_X_add_C`, `irreducible_X`, `irreducible_X_sub_C`, `irreducible_of_degree_eq_one_of_isRelPrime_coeff`, `isCoprime_X_sub_C_of_isUnit_sub`, `mem_ker_modByMonic`, `mem_nonZeroDivisors_of_leadingCoeff`, `mem_nonZeroDivisors_of_trailingCoeff`, `modByMonicHom_apply`, `natDegree_pos_of_aeval_root`, `natDegree_pos_of_monic_of_aeval_eq_zero`, `pairwise_coprime_X_sub_C`, `prime_X`, `prime_X_sub_C`, `rootMultiplicity_X_sub_C`, `rootMultiplicity_X_sub_C_pow`, `rootMultiplicity_X_sub_C_self`, `rootMultiplicity_eq_natTrailingDegree`, `rootMultiplicity_eq_rootMultiplicity`, `rootMultiplicity_mul`, `rootMultiplicity_mul'`, `rootMultiplicity_mul_X_sub_C_pow`, `smul_modByMonic`, `trailingDegree_mul`	34
Total	35

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_ne_zero_of_natDegree_ne_one` 📖	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `Ring.toSemiring`	—	—	`Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval` `not_isRoot_of_natDegree_ne_one` `FaithfulSMul.algebraMap_injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

Polynomial

Definitions

Name	Category	Theorems
`modByMonicHom` 📖	CompOp	3 math math: `modByMonicHom_apply`, `mem_ker_modByMonic`, `ker_modByMonicHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_modByMonic_eq_self_of_root` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `Ring.toSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`modByMonic` `CommRing.toRing`	—	`modByMonic_eq_sub_mul_div` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulZeroClass.zero_mul` `sub_zero`
`aeval_ne_zero_of_isCoprime` 📖	—	`IsCoprime` `Polynomial` `CommSemiring.toSemiring` `commSemiring`	—	—	`map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulZeroClass.mul_zero` `add_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `NeZero.one`
`degree_eq_degree_of_associated` 📖	mathematical	`Associated` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	`degree`	—	`degree_mul` `IsDomain.to_noZeroDivisors` `degree_coe_units` `IsDomain.toNontrivial` `add_zero`
`degree_pos_of_aeval_root` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `Nat.instMulZeroClass` `degree`	—	`natDegree_pos_iff_degree_pos` `natDegree_pos_of_aeval_root`
`exists_multiset_roots` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Multiset.card` `degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Multiset.count` `rootMultiplicity` `CommRing.toRing`	—	—
`irreducible_C_mul_X_add_C` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Irreducible` `Polynomial` `semiring` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `X`	—	`irreducible_of_degree_eq_one_of_isRelPrime_coeff` `Mathlib.Tactic.ComputeDegree.degree_eq_of_le_of_coeff_ne_zero'` `degree_add_le_of_le` `degree_mul_le_of_le` `degree_C_le` `degree_X_le` `Mathlib.Tactic.ComputeDegree.coeff_congr_lhs` `Mathlib.Tactic.ComputeDegree.coeff_add_of_eq` `Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite` `Mathlib.Tactic.ComputeDegree.natDegree_C_le` `natDegree_X_le` `coeff_C` `coeff_X` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `mul_one` `add_zero` `Nat.cast_zero` `coeff_add` `mul_coeff_zero` `coeff_C_zero` `coeff_X_zero` `MulZeroClass.mul_zero` `zero_add` `coeff_mul_X` `coeff_C_succ` `IsRelPrime.symm`
`irreducible_X` 📖	mathematical	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`Prime.irreducible` `instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `prime_X`
`irreducible_X_sub_C` 📖	mathematical	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `CommRing.toRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`Prime.irreducible` `instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `prime_X_sub_C`
`irreducible_of_degree_eq_one_of_isRelPrime_coeff` 📖	mathematical	`degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `WithBot.one` `Nat.instOne` `IsRelPrime` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `coeff`	`Irreducible` `Polynomial` `semiring`	—	`isUnit_iff` `IsDomain.to_noZeroDivisors` `not_le` `zero_lt_one'` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `NeZero.charZero_one` `WithBot.charZero` `Nat.instCharZero` `Nat.WithBot.add_eq_one_iff` `degree_mul` `eq_C_of_degree_eq_zero` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeff_C_mul` `mul_comm` `LT.lt.le`
`isCoprime_X_sub_C_of_isUnit_sub` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	`IsCoprime` `Polynomial` `commSemiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`neg_mul_comm` `left_distrib` `Distrib.leftDistribClass` `neg_add_eq_sub` `sub_sub_sub_cancel_left` `C_sub` `C_mul` `C_1` `IsUnit.val_inv_mul`
`mem_ker_modByMonic` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `modByMonicHom` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring`	—	`LinearMap.mem_ker` `modByMonic_eq_zero_iff_dvd`
`mem_nonZeroDivisors_of_leadingCoeff` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`Polynomial` `semiring`	—	`mem_nonzeroDivisors_of_coeff_mem`
`mem_nonZeroDivisors_of_trailingCoeff` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `trailingCoeff`	`Polynomial` `semiring`	—	`mem_nonzeroDivisors_of_coeff_mem`
`modByMonicHom_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `module` `Semiring.toModule` `LinearMap.instFunLike` `modByMonicHom` `modByMonic` `CommRing.toRing`	—	—
`natDegree_pos_of_aeval_root` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`natDegree`	—	`natDegree_pos_of_eval₂_root`
`natDegree_pos_of_monic_of_aeval_eq_zero` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`natDegree`	—	`natDegree_pos_of_aeval_root` `Monic.ne_zero` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective`
`pairwise_coprime_X_sub_C` 📖	mathematical	—	`Pairwise` `Function.onFun` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsCoprime` `commSemiring` `Semifield.toCommSemiring` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`isCoprime_X_sub_C_of_isUnit_sub` `Ne.isUnit` `sub_ne_zero_of_ne`
`prime_X` 📖	mathematical	—	`Prime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring` `X`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_zero` `prime_X_sub_C`
`prime_X_sub_C` 📖	mathematical	—	`Prime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring` `instSub` `CommRing.toRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`X_sub_C_ne_zero` `IsDomain.toNontrivial` `not_isUnit_X_sub_C` `eval_mul` `IsDomain.to_noZeroDivisors`
`rootMultiplicity_X_sub_C` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`rootMultiplicity_X_sub_C_self` `rootMultiplicity_eq_zero` `root_X_sub_C`
`rootMultiplicity_X_sub_C_pow` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`rootMultiplicity_mul_X_sub_C_pow` `RingHom.map_one_ne_zero` `nontrivial` `zero_add` `one_mul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `rootMultiplicity_C`
`rootMultiplicity_X_sub_C_self` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`rootMultiplicity_X_sub_C_pow` `pow_one`
`rootMultiplicity_eq_natTrailingDegree` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `comp` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`rootMultiplicity_eq_rootMultiplicity` `rootMultiplicity_eq_natTrailingDegree'`
`rootMultiplicity_eq_rootMultiplicity` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`rootMultiplicity_eq_multiplicity` `C_0` `sub_zero` `aeval_sub` `aeval_X` `AlgHom.commutes` `add_sub_cancel_right` `multiplicity_map_eq` `RingEquivClass.toMulEquivClass` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`rootMultiplicity_mul` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul`	—	`left_ne_zero_of_mul` `right_ne_zero_of_mul` `rootMultiplicity_eq_multiplicity` `multiplicity_mul` `instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `prime_X_sub_C` `finiteMultiplicity_X_sub_C`
`rootMultiplicity_mul'` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul`	—	`rootMultiplicity_eq_natTrailingDegree` `mul_comp` `natTrailingDegree_mul'` `eval_divByMonic_eq_trailingCoeff_comp`
`rootMultiplicity_mul_X_sub_C_pow` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`Monic.mul_left_ne_zero` `Monic.pow` `monic_X_sub_C` `le_antisymm` `rootMultiplicity_le_iff` `add_assoc` `add_comm` `pow_add` `dvd_cancel_right_mem_nonZeroDivisors` `Monic.mem_nonZeroDivisors` `pow_rootMultiplicity_not_dvd` `le_rootMultiplicity_iff` `mul_dvd_mul_right` `pow_rootMultiplicity_dvd`
`smul_modByMonic` 📖	mathematical	—	`modByMonic` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.toSMul` `semiring` `algebraOfAlgebra` `Algebra.id` `Ring.toSemiring`	—	`subsingleton_or_nontrivial` `Unique.instSubsingleton` `div_modByMonic_unique` `mul_smul_comm` `Algebra.to_smulCommClass` `smul_add` `modByMonic_add_div` `LE.le.trans_lt` `degree_smul_le` `degree_modByMonic_lt` `modByMonic_eq_of_not_monic`
`trailingDegree_mul` 📖	mathematical	—	`trailingDegree` `Polynomial` `instMul` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`MulZeroClass.zero_mul` `trailingDegree_zero` `top_add` `MulZeroClass.mul_zero` `add_top` `trailingDegree_eq_natTrailingDegree` `mul_ne_zero` `instNoZeroDivisors` `natTrailingDegree_mul` `WithTop.coe_add`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_of_degree_eq_one` 📖	mathematical	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `WithBot.one` `Nat.instOne` `Polynomial.Monic`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	—	`Prime.irreducible` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `prime_of_degree_eq_one`
`mem_nonZeroDivisors` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Polynomial.semiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`Polynomial.mem_nonzeroDivisors_of_coeff_mem` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `coeff_natDegree`
`neg_one_pow_natDegree_mul_comp_neg_X` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Polynomial` `Polynomial.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instNeg` `CommRing.toRing` `Polynomial.instOne` `Polynomial.natDegree` `Polynomial.comp` `Polynomial.X`	—	`mul_comm` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_neg` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one` `Polynomial.comp_neg_X_leadingCoeff_eq` `leadingCoeff` `mul_one` `Even.neg_pow` `one_pow`
`prime_of_degree_eq_one` 📖	mathematical	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `WithBot.one` `Nat.instOne` `Polynomial.Monic`	`Prime` `Polynomial` `CommSemiring.toCommMonoidWithZero` `Polynomial.commSemiring`	—	`map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_neg_eq_add` `leadingCoeff` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_mul` `Polynomial.eq_X_add_C_of_degree_eq_one` `Polynomial.prime_X_sub_C`

---

← Back to Index