Operations

📁 Source: Mathlib/Algebra/Polynomial/Degree/Operations.lean

Statistics

Metric	Count
Definitions `degreeMonoidHom`, `instWellFoundedRelation`, `leadingCoeffHom`	3
Theorems `degree_mul`, `degree_pos`, `leadingCoeff_C_mul`, `natDegree_eq_zero`, `natDegree_pos`, `X_add_C_ne_one`, `X_add_C_ne_zero`, `X_pow_add_C_ne_one`, `X_pow_add_C_ne_zero`, `X_pow_sub_C_ne_zero`, `X_sub_C_ne_zero`, `coeff_X_sub_C_mul`, `coeff_eq_zero_of_degree_lt`, `coeff_eq_zero_of_natDegree_lt`, `coeff_mul_X_sub_C`, `coeff_mul_add_eq_of_natDegree_le`, `coeff_mul_degree_add_degree`, `coeff_natDegree_eq_zero_of_degree_lt`, `coeff_natDegree_succ_eq_zero`, `coeff_pow_mul_natDegree`, `degree_C_lt_degree_C_mul_X`, `degree_C_mul_of_isUnit`, `degree_X_add_C`, `degree_X_pow_add_C`, `degree_X_pow_sub_C`, `degree_X_sub_C`, `degree_add_C`, `degree_add_eq_left_of_degree_lt`, `degree_add_eq_of_leadingCoeff_add_ne_zero`, `degree_add_eq_right_of_degree_lt`, `degree_eq_of_le_of_coeff_ne_zero`, `degree_le_mul_left`, `degree_le_zero_iff`, `degree_lt_degree`, `degree_lt_degree_mul_X`, `degree_lt_wf`, `degree_mul`, `degree_mul'`, `degree_mul_C_of_isUnit`, `degree_mul_X`, `degree_mul_X_pow`, `degree_of_subsingleton`, `degree_pow`, `degree_pow'`, `degree_smul_le`, `degree_smul_of_isRightRegular_leadingCoeff`, `degree_sub_C`, `degree_sub_eq_left_of_degree_lt`, `degree_sub_eq_right_of_degree_lt`, `degree_sum_fin_lt`, `eq_C_coeff_zero_iff_natDegree_eq_zero`, `eq_C_of_degree_eq_zero`, `eq_C_of_degree_le_zero`, `eq_C_of_natDegree_eq_zero`, `eq_C_of_natDegree_le_zero`, `eq_one_of_monic_natDegree_zero`, `ext_iff_degree_le`, `ext_iff_natDegree_le`, `ite_le_natDegree_coeff`, `le_natDegree_of_ne_zero`, `leadingCoeffHom_apply`, `leadingCoeff_C_mul_of_isUnit`, `leadingCoeff_X_add_C`, `leadingCoeff_X_pow_add_C`, `leadingCoeff_X_pow_add_one`, `leadingCoeff_X_pow_sub_C`, `leadingCoeff_X_pow_sub_one`, `leadingCoeff_X_sub_C`, `leadingCoeff_add_of_degree_eq`, `leadingCoeff_add_of_degree_lt`, `leadingCoeff_add_of_degree_lt'`, `leadingCoeff_dvd_leadingCoeff`, `leadingCoeff_monic_mul`, `leadingCoeff_mul`, `leadingCoeff_mul'`, `leadingCoeff_mul_C_of_isUnit`, `leadingCoeff_mul_X`, `leadingCoeff_mul_X_pow`, `leadingCoeff_mul_monic`, `leadingCoeff_pow`, `leadingCoeff_pow'`, `leadingCoeff_pow_X_add_C`, `leadingCoeff_sub_of_degree_eq`, `leadingCoeff_sub_of_degree_lt`, `leadingCoeff_sub_of_degree_lt'`, `monic_of_degree_le`, `monic_of_degree_le_of_coeff_eq_one`, `monic_of_natDegree_le_of_coeff_eq_one`, `monic_of_subsingleton`, `natDegree_C_add`, `natDegree_C_mul_of_isUnit`, `natDegree_X_add_C`, `natDegree_X_mul`, `natDegree_X_pow_add_C`, `natDegree_X_pow_le`, `natDegree_X_pow_mul`, `natDegree_X_pow_sub_C`, `natDegree_X_sub_C`, `natDegree_add_C`, `natDegree_add_eq_left_of_degree_lt`, `natDegree_add_eq_left_of_natDegree_lt`, `natDegree_add_eq_right_of_degree_lt`, `natDegree_add_eq_right_of_natDegree_lt`, `natDegree_eq_natDegree`, `natDegree_eq_of_le_of_coeff_ne_zero`, `natDegree_eq_of_natDegree_add_eq_zero`, `natDegree_eq_of_natDegree_add_lt_left`, `natDegree_eq_of_natDegree_add_lt_right`, `natDegree_eq_zero`, `natDegree_lt_natDegree`, `natDegree_lt_natDegree_iff`, `natDegree_mul'`, `natDegree_mul_C_of_isUnit`, `natDegree_mul_X`, `natDegree_mul_X_pow`, `natDegree_of_subsingleton`, `natDegree_pow'`, `natDegree_smul_le`, `natDegree_sub_C`, `natDegree_sub_eq_left_of_natDegree_lt`, `natDegree_sub_eq_right_of_natDegree_lt`, `ne_zero_of_degree_ge_degree`, `ne_zero_of_degree_gt`, `ne_zero_of_natDegree_gt`, `nextCoeff_X_add_C`, `nextCoeff_X_sub_C`, `not_isUnit_X`, `supDegree_eq_degree`, `zero_notMem_multiset_map_X_add_C`, `zero_notMem_multiset_map_X_sub_C`	130
Total	133

Polynomial

Definitions

Name	Category	Theorems
`degreeMonoidHom` 📖	CompOp	—
`instWellFoundedRelation` 📖	CompOp	—
`leadingCoeffHom` 📖	CompOp	1 math math: `leadingCoeffHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_add_C_ne_one` 📖	—	—	—	—	`X_pow_add_C_ne_one` `zero_lt_one` `Nat.instZeroLEOneClass` `pow_one`
`X_add_C_ne_zero` 📖	—	—	—	—	`X_pow_add_C_ne_zero` `zero_lt_one` `Nat.instZeroLEOneClass` `pow_one`
`X_pow_add_C_ne_one` 📖	—	—	—	—	`LT.lt.ne'` `natDegree_X_pow_add_C` `natDegree_one`
`X_pow_add_C_ne_zero` 📖	—	—	—	—	`degree_eq_bot` `degree_X_pow_add_C` `WithBot.coe_ne_bot`
`X_pow_sub_C_ne_zero` 📖	—	—	—	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `X_pow_add_C_ne_zero`
`X_sub_C_ne_zero` 📖	—	—	—	—	`X_pow_sub_C_ne_zero` `zero_lt_one` `Nat.instZeroLEOneClass` `pow_one`
`coeff_X_sub_C_mul` 📖	mathematical	—	`coeff` `Ring.toSemiring` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`sub_mul` `coeff_sub` `coeff_X_mul` `coeff_C_mul`
`coeff_eq_zero_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`le_degree_of_ne_zero` `not_le_of_gt`
`coeff_eq_zero_of_natDegree_lt` 📖	mathematical	`natDegree`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_degree_lt` `WithBot.bot_lt_coe` `degree_eq_natDegree` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`coeff_mul_X_sub_C` 📖	mathematical	—	`coeff` `Ring.toSemiring` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`mul_sub` `coeff_sub` `coeff_mul_X` `coeff_mul_C`
`coeff_mul_add_eq_of_natDegree_le` 📖	mathematical	`natDegree`	`coeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_mul` `Finset.sum_eq_single_of_mem` `Finset.HasAntidiagonal.mem_antidiagonal` `lt_or_ge` `coeff_eq_zero_of_natDegree_lt` `LE.le.trans_lt` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `add_eq_add_iff_eq_and_eq` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`coeff_mul_degree_add_degree` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `natDegree` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `leadingCoeff`	—	`coeff_mul` `Finset.sum_eq_single` `coeff_eq_zero_of_degree_lt` `lt_of_le_of_lt` `degree_le_natDegree` `WithBot.coe_lt_coe` `MulZeroClass.zero_mul` `not_lt_iff_eq_or_lt` `Finset.HasAntidiagonal.mem_antidiagonal` `ne_of_lt` `MulZeroClass.mul_zero`
`coeff_natDegree_eq_zero_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`coeff` `natDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `degree_le_natDegree`
`coeff_natDegree_succ_eq_zero` 📖	mathematical	—	`coeff` `natDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_natDegree_lt` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`coeff_pow_mul_natDegree` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `natDegree` `leadingCoeff`	—	`pow_zero` `MulZeroClass.zero_mul` `coeff_one_zero` `pow_succ` `coeff_zero` `coeff_eq_zero_of_natDegree_lt` `lt_of_le_of_ne` `natDegree_pow_le` `leadingCoeff_eq_zero` `natDegree_mul_le` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `natDegree_pow'` `leadingCoeff_pow'` `coeff_mul_degree_add_degree`
`degree_C_lt_degree_C_mul_X` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instMul` `X`	—	`degree_C_mul_X` `degree_C_lt`
`degree_C_mul_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`degree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`eq_or_ne` `MulZeroClass.mul_zero` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `degree_of_subsingleton` `degree_mul'` `leadingCoeff_C` `IsUnit.mul_right_eq_zero` `degree_C` `IsUnit.ne_zero` `zero_add`
`degree_X_add_C` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `WithBot` `WithBot.one` `Nat.instOne`	—	`degree_C_le` `WithBot.coe_lt_coe` `zero_lt_one` `Nat.instZeroLEOneClass` `degree_X` `degree_add_eq_left_of_degree_lt`
`degree_X_pow_add_C` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`LE.le.trans_lt` `degree_C_le` `degree_X_pow` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Nat.cast_pos` `WithBot.instIsOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `WithBot.nontrivial` `degree_add_eq_left_of_degree_lt`
`degree_X_pow_sub_C` 📖	mathematical	—	`degree` `Ring.toSemiring` `Polynomial` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `degree_X_pow_add_C`
`degree_X_sub_C` 📖	mathematical	—	`degree` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `WithBot` `WithBot.one` `Nat.instOne`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `degree_X_add_C`
`degree_add_C` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree`	`Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`degree_add_eq_right_of_degree_lt` `add_comm` `lt_of_le_of_lt` `degree_C_le`
`degree_add_eq_left_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`Polynomial` `instAdd`	—	`le_antisymm` `degree_add_le` `max_eq_left_of_lt` `degree_le_degree` `coeff_add` `coeff_natDegree_eq_zero_of_degree_lt` `add_zero` `leadingCoeff_eq_zero` `ne_zero_of_degree_gt`
`degree_add_eq_of_leadingCoeff_add_ne_zero` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `WithBot` `SemilatticeSup.toMax` `WithBot.semilatticeSup` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeNat`	—	`le_antisymm` `degree_add_le` `lt_trichotomy` `degree_add_eq_right_of_degree_lt` `max_eq_right_of_lt` `le_refl` `le_of_not_gt` `leadingCoeff.eq_1` `natDegree_eq_of_degree_eq` `coeff_add` `coeff_natDegree_eq_zero_of_degree_lt` `max_self` `degree_add_eq_left_of_degree_lt` `max_eq_left_of_lt`
`degree_add_eq_right_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`Polynomial` `instAdd`	—	`add_comm` `degree_add_eq_left_of_degree_lt`
`degree_eq_of_le_of_coeff_ne_zero` 📖	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	—	`LE.le.antisymm` `le_degree_of_ne_zero`
`degree_le_mul_left` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instMul`	—	`eq_or_ne` `MulZeroClass.zero_mul` `degree_mul` `degree_eq_natDegree` `WithBot.coe_le_coe`
`degree_le_zero_iff` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`eq_C_of_degree_le_zero` `degree_C_le`
`degree_lt_degree` 📖	mathematical	`natDegree`	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	`bot_lt_iff_ne_bot` `degree_eq_bot` `degree_eq_natDegree` `ne_zero_of_natDegree_gt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`degree_lt_degree_mul_X` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instMul` `X`	—	`Monic.leadingCoeff` `mul_one` `degree_mul'` `degree_eq_natDegree` `degree_X` `Nontrivial.of_polynomial_ne` `Nat.cast_one` `Nat.cast_add` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`degree_lt_wf` 📖	mathematical	—	`Polynomial` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	`wellFounded_lt` `WithBot.instWellFoundedLT` `instWellFoundedLTNat`
`degree_mul` 📖	mathematical	—	`degree` `Polynomial` `instMul` `WithBot` `WithBot.add`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `WithBot.add_bot` `degree_mul'` `mul_ne_zero` `leadingCoeff_eq_zero`
`degree_mul'` 📖	mathematical	—	`degree` `Polynomial` `instMul` `WithBot` `WithBot.add`	—	`leadingCoeff_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `le_antisymm` `degree_mul_le` `degree_eq_natDegree` `le_degree_of_ne_zero` `coeff_mul_degree_add_degree`
`degree_mul_C_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`degree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`eq_or_ne` `MulZeroClass.zero_mul` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `degree_of_subsingleton` `degree_mul'` `leadingCoeff_C` `IsUnit.mul_left_eq_zero` `degree_C` `IsUnit.ne_zero` `add_zero`
`degree_mul_X` 📖	mathematical	—	`degree` `Polynomial` `instMul` `X` `WithBot` `WithBot.add` `WithBot.one` `Nat.instOne`	—	`Monic.degree_mul` `monic_X` `degree_X`
`degree_mul_X_pow` 📖	mathematical	—	`degree` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `WithBot` `WithBot.add` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`Monic.degree_mul` `monic_X_pow` `degree_X_pow`
`degree_of_subsingleton` 📖	mathematical	—	`degree` `Bot.bot` `WithBot` `WithBot.bot`	—	`Unique.instSubsingleton` `degree_zero`
`degree_pow` 📖	mathematical	—	`degree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `WithBot` `AddMonoid.toNatSMul` `WithBot.addMonoid` `Nat.instAddMonoid`	—	`map_pow` `MonoidHom.instMonoidHomClass`
`degree_pow'` 📖	mathematical	—	`degree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `WithBot` `AddMonoid.toNatSMul` `WithBot.addMonoid` `Nat.instAddMonoid`	—	`pow_zero` `C_1` `degree_C` `zero_nsmul` `pow_succ` `MulZeroClass.zero_mul` `leadingCoeff_pow'` `degree_mul'` `succ_nsmul`
`degree_smul_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`degree_le_iff_coeff_zero` `coeff_smul` `degree_lt_iff_coeff_zero` `le_rfl` `smul_zero`
`degree_smul_of_isRightRegular_leadingCoeff` 📖	mathematical	`IsRightRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `leadingCoeff`	`degree` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul`	—	`le_antisymm` `degree_smul_le` `degree_le_degree` `coeff_smul` `coeff_natDegree` `smul_eq_mul` `Iff.ne` `IsRightRegular.mul_right_eq_zero_iff`
`degree_sub_C` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Ring.toSemiring`	`Polynomial` `instSub` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`sub_eq_add_neg` `C_neg` `degree_add_C`
`degree_sub_eq_left_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring`	`Polynomial` `instSub`	—	`sub_eq_add_neg` `degree_add_eq_left_of_degree_lt` `degree_neg`
`degree_sub_eq_right_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring`	`Polynomial` `instSub`	—	`sub_eq_add_neg` `degree_add_eq_right_of_degree_lt` `degree_neg`
`degree_sum_fin_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `Finset.univ` `Fin.fintype` `instMul` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`LE.le.trans_lt` `degree_sum_le` `Finset.sup_lt_iff` `WithBot.bot_lt_coe` `degree_C_mul_X_pow_le` `WithBot.coe_lt_coe`
`eq_C_coeff_zero_iff_natDegree_eq_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff` `natDegree`	—	`natDegree_C` `eq_C_of_natDegree_eq_zero`
`eq_C_of_degree_eq_zero` 📖	mathematical	`degree` `WithBot` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`eq_C_of_degree_le_zero` `Eq.le`
`eq_C_of_degree_le_zero` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`ext` `coeff_C_zero` `coeff_C` `coeff_eq_zero_of_degree_lt` `LE.le.trans_lt` `WithBot.coe_lt_coe`
`eq_C_of_natDegree_eq_zero` 📖	mathematical	`natDegree`	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`eq_C_of_natDegree_le_zero` `Eq.le`
`eq_C_of_natDegree_le_zero` 📖	mathematical	`natDegree`	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`eq_C_of_degree_le_zero` `degree_le_of_natDegree_le`
`eq_one_of_monic_natDegree_zero` 📖	mathematical	`Monic` `natDegree`	`Polynomial` `instOne`	—	`eq_C_of_natDegree_eq_zero` `leadingCoeff.eq_1` `Monic.def` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`ext_iff_degree_le` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	`coeff`	—	`ext_iff_natDegree_le` `natDegree_le_of_degree_le`
`ext_iff_natDegree_le` 📖	mathematical	`natDegree`	`coeff`	—	`ext_iff` `le_or_gt` `coeff_eq_zero_of_natDegree_lt` `LE.le.trans_lt`
`ite_le_natDegree_coeff` 📖	mathematical	—	`natDegree` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_eq_zero_of_natDegree_lt` `not_le`
`le_natDegree_of_ne_zero` 📖	mathematical	—	`natDegree`	—	`Nat.cast_le` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `degree_eq_natDegree` `le_degree_of_ne_zero`
`leadingCoeffHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Polynomial` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `semiring` `MonoidHom.instFunLike` `leadingCoeffHom` `leadingCoeff`	—	—
`leadingCoeff_C_mul_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`leadingCoeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`leadingCoeff.eq_1` `coeff_C_mul` `natDegree_C_mul_of_isUnit`
`leadingCoeff_X_add_C` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`pow_one` `leadingCoeff_X_pow_add_C` `zero_lt_one` `Nat.instZeroLEOneClass`
`leadingCoeff_X_pow_add_C` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Monic.leadingCoeff` `leadingCoeff.eq_1` `natDegree_X_pow_add_C` `coeff_add` `coeff_X_pow_self` `coeff_C` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `add_zero`
`leadingCoeff_X_pow_add_one` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`leadingCoeff_X_pow_add_C`
`leadingCoeff_X_pow_sub_C` 📖	mathematical	—	`leadingCoeff` `Ring.toSemiring` `Polynomial` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `leadingCoeff_X_pow_add_C`
`leadingCoeff_X_pow_sub_one` 📖	mathematical	—	`leadingCoeff` `Ring.toSemiring` `Polynomial` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`leadingCoeff_X_pow_sub_C`
`leadingCoeff_X_sub_C` 📖	mathematical	—	`leadingCoeff` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `leadingCoeff_X_add_C`
`leadingCoeff_add_of_degree_eq` 📖	mathematical	`degree`	`leadingCoeff` `Polynomial` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`natDegree_eq_of_degree_eq` `degree_add_eq_of_leadingCoeff_add_ne_zero` `max_self` `coeff_add`
`leadingCoeff_add_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`leadingCoeff` `Polynomial` `instAdd`	—	`coeff_natDegree_eq_zero_of_degree_lt` `natDegree_eq_of_degree_eq` `degree_add_eq_right_of_degree_lt` `coeff_add` `zero_add`
`leadingCoeff_add_of_degree_lt'` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`leadingCoeff` `Polynomial` `instAdd`	—	`add_comm` `leadingCoeff_add_of_degree_lt`
`leadingCoeff_dvd_leadingCoeff` 📖	mathematical	`Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `semiring`	`leadingCoeff`	—	`map_dvd` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`leadingCoeff_monic_mul` 📖	mathematical	`Monic`	`leadingCoeff` `Polynomial` `instMul`	—	`eq_or_ne` `MulZeroClass.mul_zero` `leadingCoeff_mul'` `Monic.leadingCoeff` `one_mul` `leadingCoeff_eq_zero`
`leadingCoeff_mul` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `leadingCoeff_mul'` `mul_ne_zero` `leadingCoeff_eq_zero`
`leadingCoeff_mul'` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`natDegree_mul'` `coeff_mul_degree_add_degree`
`leadingCoeff_mul_C_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`leadingCoeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`leadingCoeff.eq_1` `coeff_mul_C` `natDegree_mul_C_of_isUnit`
`leadingCoeff_mul_X` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instMul` `X`	—	`leadingCoeff_mul_monic` `monic_X`
`leadingCoeff_mul_X_pow` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`leadingCoeff_mul_monic` `monic_X_pow`
`leadingCoeff_mul_monic` 📖	mathematical	`Monic`	`leadingCoeff` `Polynomial` `instMul`	—	`leadingCoeff_eq_zero` `MulZeroClass.zero_mul` `leadingCoeff_zero` `leadingCoeff_mul'` `Monic.leadingCoeff` `mul_one`
`leadingCoeff_pow` 📖	mathematical	—	`leadingCoeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`MonoidHom.map_pow`
`leadingCoeff_pow'` 📖	mathematical	—	`leadingCoeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`pow_zero` `Monic.leadingCoeff` `pow_succ` `MulZeroClass.zero_mul` `pow_succ'` `leadingCoeff_mul'`
`leadingCoeff_pow_X_add_C` 📖	mathematical	—	`leadingCoeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Monic.leadingCoeff` `leadingCoeff_pow'` `leadingCoeff_X_add_C` `one_pow` `NeZero.one`
`leadingCoeff_sub_of_degree_eq` 📖	mathematical	`degree` `Ring.toSemiring`	`leadingCoeff` `Polynomial` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`degree_neg` `leadingCoeff_neg` `sub_eq_add_neg` `sub_ne_zero` `leadingCoeff_add_of_degree_eq`
`leadingCoeff_sub_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring`	`leadingCoeff` `Polynomial` `instSub`	—	`sub_eq_add_neg` `leadingCoeff_add_of_degree_lt'` `degree_neg`
`leadingCoeff_sub_of_degree_lt'` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Ring.toSemiring`	`leadingCoeff` `Polynomial` `instSub` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`sub_eq_add_neg` `leadingCoeff_add_of_degree_lt` `degree_neg` `leadingCoeff_neg`
`monic_of_degree_le` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `coeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Monic`	—	`monic_of_natDegree_le_of_coeff_eq_one` `natDegree_le_of_degree_le`
`monic_of_degree_le_of_coeff_eq_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `coeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Monic`	—	`monic_of_degree_le`
`monic_of_natDegree_le_of_coeff_eq_one` 📖	mathematical	`natDegree` `coeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Monic`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Monic.leadingCoeff` `natDegree_eq_of_le_of_coeff_ne_zero` `ne_of_eq_of_ne` `one_ne_zero` `NeZero.one`
`monic_of_subsingleton` 📖	mathematical	—	`Monic`	—	—
`natDegree_C_add` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`add_comm` `natDegree_add_C`
`natDegree_C_mul_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`natDegree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`degree_C_mul_of_isUnit`
`natDegree_X_add_C` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`natDegree_eq_of_degree_eq_some` `degree_X_add_C`
`natDegree_X_mul` 📖	mathematical	—	`natDegree` `Polynomial` `instMul` `X`	—	`commute_X` `natDegree_mul_X`
`natDegree_X_pow_add_C` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`natDegree_add_C` `natDegree_X_pow`
`natDegree_X_pow_le` 📖	mathematical	—	`natDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `natDegree_of_subsingleton` `Nat.instCanonicallyOrderedAdd` `natDegree_X_pow` `le_refl`
`natDegree_X_pow_mul` 📖	mathematical	—	`natDegree` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`commute_X_pow` `natDegree_mul_X_pow`
`natDegree_X_pow_sub_C` 📖	mathematical	—	`natDegree` `Ring.toSemiring` `Polynomial` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `natDegree_X_pow_add_C`
`natDegree_X_sub_C` 📖	mathematical	—	`natDegree` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`natDegree_sub_C` `natDegree_X`
`natDegree_add_C` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`eq_or_ne` `zero_add` `natDegree_C` `eq_C_of_degree_le_zero` `C_add` `natDegree_add_eq_left_of_natDegree_lt` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Nat.cast_pos` `WithBot.instIsOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `WithBot.nontrivial` `degree_eq_natDegree`
`natDegree_add_eq_left_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`natDegree` `Polynomial` `instAdd`	—	`natDegree_eq_of_degree_eq` `degree_add_eq_left_of_degree_lt`
`natDegree_add_eq_left_of_natDegree_lt` 📖	mathematical	`natDegree`	`Polynomial` `instAdd`	—	`natDegree_add_eq_left_of_degree_lt` `degree_lt_degree`
`natDegree_add_eq_right_of_degree_lt` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`natDegree` `Polynomial` `instAdd`	—	`natDegree_eq_of_degree_eq` `degree_add_eq_right_of_degree_lt`
`natDegree_add_eq_right_of_natDegree_lt` 📖	mathematical	`natDegree`	`Polynomial` `instAdd`	—	`natDegree_add_eq_right_of_degree_lt` `degree_lt_degree`
`natDegree_eq_natDegree` 📖	mathematical	`degree`	`natDegree`	—	—
`natDegree_eq_of_le_of_coeff_ne_zero` 📖	—	`natDegree`	—	—	`LE.le.antisymm` `le_natDegree_of_ne_zero`
`natDegree_eq_of_natDegree_add_eq_zero` 📖	—	`natDegree` `Polynomial` `instAdd`	—	—	`natDegree_eq_of_natDegree_add_lt_right` `natDegree_eq_of_natDegree_add_lt_left`
`natDegree_eq_of_natDegree_add_lt_left` 📖	—	`natDegree` `Polynomial` `instAdd`	—	—	`lt_asymm` `natDegree_add_eq_right_of_natDegree_lt` `LT.lt.false` `natDegree_add_eq_left_of_natDegree_lt`
`natDegree_eq_of_natDegree_add_lt_right` 📖	—	`natDegree` `Polynomial` `instAdd`	—	—	`natDegree_eq_of_natDegree_add_lt_left` `add_comm`
`natDegree_eq_zero` 📖	mathematical	—	`natDegree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`eq_C_of_natDegree_eq_zero` `natDegree_C`
`natDegree_lt_natDegree` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`natDegree`	—	`not_lt_bot` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `degree_eq_natDegree`
`natDegree_lt_natDegree_iff` 📖	mathematical	—	`natDegree` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	`degree_lt_degree` `ne_zero_of_degree_gt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `degree_eq_natDegree`
`natDegree_mul'` 📖	mathematical	—	`natDegree` `Polynomial` `instMul`	—	`leadingCoeff_eq_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `natDegree_eq_of_degree_eq_some` `degree_mul'` `Nat.cast_add` `degree_eq_natDegree`
`natDegree_mul_C_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`natDegree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`degree_mul_C_of_isUnit`
`natDegree_mul_X` 📖	mathematical	—	`natDegree` `Polynomial` `instMul` `X`	—	`natDegree_mul'` `Monic.leadingCoeff` `mul_one` `natDegree_X`
`natDegree_mul_X_pow` 📖	mathematical	—	`natDegree` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`natDegree_mul'` `Monic.leadingCoeff` `mul_one` `natDegree_X_pow`
`natDegree_of_subsingleton` 📖	mathematical	—	`natDegree`	—	`Unique.instSubsingleton` `natDegree_zero`
`natDegree_pow'` 📖	mathematical	—	`natDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`pow_zero` `natDegree_one` `MulZeroClass.mul_zero` `zero_pow` `leadingCoeff_zero` `leadingCoeff_pow'` `degree_eq_natDegree` `degree_pow'` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `nsmul_eq_mul` `Nat.cast_mul`
`natDegree_smul_le` 📖	mathematical	—	`natDegree` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`natDegree_le_natDegree` `degree_smul_le`
`natDegree_sub_C` 📖	mathematical	—	`natDegree` `Ring.toSemiring` `Polynomial` `instSub` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`sub_eq_add_neg` `C_neg` `natDegree_add_C`
`natDegree_sub_eq_left_of_natDegree_lt` 📖	mathematical	`natDegree` `Ring.toSemiring`	`Polynomial` `instSub`	—	`natDegree_eq_of_degree_eq` `degree_sub_eq_left_of_degree_lt` `degree_lt_degree`
`natDegree_sub_eq_right_of_natDegree_lt` 📖	mathematical	`natDegree` `Ring.toSemiring`	`Polynomial` `instSub`	—	`natDegree_eq_of_degree_eq` `degree_sub_eq_right_of_degree_lt` `degree_lt_degree`
`ne_zero_of_degree_ge_degree` 📖	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	—	`ne_zero_of_degree_gt` `lt_of_lt_of_le` `bot_lt_iff_ne_bot` `degree_eq_bot`
`ne_zero_of_degree_gt` 📖	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	—	`degree_eq_bot` `LT.lt.ne_bot`
`ne_zero_of_natDegree_gt` 📖	—	`natDegree`	—	—	`Nat.instCanonicallyOrderedAdd`
`nextCoeff_X_add_C` 📖	mathematical	—	`nextCoeff` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `nextCoeff_of_natDegree_pos` `natDegree_add_C` `natDegree_X` `Nat.instZeroLEOneClass` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `coeff_add` `coeff_X_zero` `coeff_C_zero` `zero_add`
`nextCoeff_X_sub_C` 📖	mathematical	—	`nextCoeff` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `nextCoeff_X_add_C`
`not_isUnit_X` 📖	mathematical	—	`IsUnit` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`zero_ne_one'` `NeZero.one` `coeff_one_zero` `mul_coeff_zero` `coeff_monomial_succ` `MulZeroClass.mul_zero`
`supDegree_eq_degree` 📖	mathematical	—	`AddMonoidAlgebra.supDegree` `WithBot` `WithBot.semilatticeSup` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeNat` `WithBot.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `WithBot.some` `toFinsupp` `degree`	—	`Finset.max_eq_sup_coe`
`zero_notMem_multiset_map_X_add_C` 📖	mathematical	—	`Polynomial` `Multiset` `Multiset.instMembership` `Multiset.map` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instZero`	—	`Multiset.mem_map` `X_add_C_ne_zero`
`zero_notMem_multiset_map_X_sub_C` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `Multiset` `Multiset.instMembership` `Multiset.map` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instZero`	—	`Multiset.mem_map` `X_sub_C_ne_zero`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_mul` 📖	mathematical	`Polynomial.Monic`	`Polynomial.degree` `Polynomial` `Polynomial.instMul` `WithBot` `WithBot.add`	—	`MulZeroClass.zero_mul` `Polynomial.degree_mul'` `leadingCoeff` `mul_one` `Polynomial.leadingCoeff_eq_zero`
`degree_pos` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring`	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Polynomial.degree`	—	`Polynomial.natDegree_pos_iff_degree_pos` `natDegree_pos`
`leadingCoeff_C_mul` 📖	mathematical	`Polynomial.Monic`	`Polynomial.leadingCoeff` `Polynomial` `Polynomial.instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `Polynomial.leadingCoeff_mul'` `Polynomial.leadingCoeff_C` `leadingCoeff` `mul_one`
`natDegree_eq_zero` 📖	mathematical	`Polynomial.Monic`	`Polynomial.natDegree` `Polynomial` `Polynomial.instOne`	—	`Polynomial.eq_one_of_monic_natDegree_zero` `Polynomial.natDegree_one`
`natDegree_pos` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring`	`Polynomial.natDegree`	—	`Iff.not` `natDegree_eq_zero`

---

← Back to Index