IsMonicOfDegree

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

Statistics

Metric	Count
Definitions `IsMonicOfDegree`	1
Theorems `add_left`, `add_right`, `aeval_add`, `aeval_sub`, `coeff_eq`, `comp`, `exists_natDegree_lt`, `leadingCoeff_eq`, `monic`, `mul`, `natDegree_eq`, `natDegree_sub_X_pow`, `natDegree_sub_lt`, `ne_zero`, `of_dvd_add`, `of_dvd_sub`, `of_mul_left`, `of_mul_right`, `pow`, `sub`, `isMonicOfDegree_X`, `isMonicOfDegree_X_add_one`, `isMonicOfDegree_X_pow`, `isMonicOfDegree_X_sub_one`, `isMonicOfDegree_add_add_two`, `isMonicOfDegree_iff`, `isMonicOfDegree_iff'`, `isMonicOfDegree_iff_of_subsingleton`, `isMonicOfDegree_monomial_one`, `isMonicOfDegree_one_iff`, `isMonicOfDegree_sub_add_two`, `isMonicOfDegree_two_iff`, `isMonicOfDegree_two_iff'`, `isMonicOfDegree_zero_iff`	34
Total	35

Polynomial

Definitions

Name	Category	Theorems
`IsMonicOfDegree` 📖	CompData	15 math math: `isMonicOfDegree_X_add_one`, `isMonicOfDegree_iff`, `isMonicOfDegree_two_iff'`, `isMonicOfDegree_X_sub_one`, `isMonicOfDegree_add_add_two`, `isMonicOfDegree_two_iff`, `isMonicOfDegree_zero_iff`, `isMonicOfDegree_iff'`, `isMonicOfDegree_one_iff`, `NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero`, `isMonicOfDegree_monomial_one`, `isMonicOfDegree_X_pow`, `isMonicOfDegree_X`, `isMonicOfDegree_iff_of_subsingleton`, `isMonicOfDegree_sub_add_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMonicOfDegree_X` 📖	mathematical	—	`IsMonicOfDegree` `X`	—	`isMonicOfDegree_iff` `natDegree_X_le` `coeff_X_one`
`isMonicOfDegree_X_add_one` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`IsMonicOfDegree.add_right` `isMonicOfDegree_X` `natDegree_C` `zero_lt_one` `Nat.instZeroLEOneClass`
`isMonicOfDegree_X_pow` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`isMonicOfDegree_iff` `natDegree_X_pow_le` `coeff_X_pow_self`
`isMonicOfDegree_X_sub_one` 📖	mathematical	—	`IsMonicOfDegree` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`IsMonicOfDegree.sub` `isMonicOfDegree_X` `natDegree_C` `zero_lt_one` `Nat.instZeroLEOneClass`
`isMonicOfDegree_add_add_two` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`add_assoc` `IsMonicOfDegree.add_right` `isMonicOfDegree_X_pow` `natDegree_add_le` `natDegree_C` `sup_of_le_left` `Nat.instCanonicallyOrderedAdd` `LE.le.trans_lt` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `natDegree_C_mul_le` `natDegree_X_le` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`isMonicOfDegree_iff` 📖	mathematical	—	`IsMonicOfDegree` `natDegree` `coeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Eq.le` `Monic.coeff_natDegree` `natDegree_eq_of_le_of_coeff_ne_zero` `one_ne_zero` `NeZero.one` `monic_of_natDegree_le_of_coeff_eq_one`
`isMonicOfDegree_iff'` 📖	mathematical	—	`IsMonicOfDegree` `natDegree` `Monic`	—	—
`isMonicOfDegree_iff_of_subsingleton` 📖	mathematical	—	`IsMonicOfDegree`	—	`Subsingleton.eq_one` `Unique.instSubsingleton` `natDegree_one` `isMonicOfDegree_zero_iff`
`isMonicOfDegree_monomial_one` 📖	mathematical	—	`IsMonicOfDegree` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`monomial_one_right_eq_X_pow` `isMonicOfDegree_X_pow`
`isMonicOfDegree_one_iff` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`ext` `coeff_add` `coeff_X_zero` `coeff_C_zero` `zero_add` `IsMonicOfDegree.coeff_eq` `isMonicOfDegree_X_add_one`
`isMonicOfDegree_sub_add_two` 📖	mathematical	—	`IsMonicOfDegree` `Ring.toSemiring` `Polynomial` `instAdd` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`sub_add` `IsMonicOfDegree.add_right` `isMonicOfDegree_X_pow` `natDegree_neg` `natDegree_sub_le` `natDegree_C` `sup_of_le_left` `Nat.instCanonicallyOrderedAdd` `LE.le.trans_lt` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `natDegree_C_mul_le` `natDegree_X_le` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`isMonicOfDegree_two_iff` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`ext` `lt_trichotomy` `coeff_add` `coeff_X_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `mul_coeff_zero` `coeff_C_zero` `coeff_X_zero` `MulZeroClass.mul_zero` `add_zero` `zero_add` `coeff_mul_X` `coeff_C_succ` `IsMonicOfDegree.coeff_eq` `isMonicOfDegree_add_add_two`
`isMonicOfDegree_two_iff'` 📖	mathematical	—	`IsMonicOfDegree` `Ring.toSemiring` `Polynomial` `instAdd` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`sub_eq_add_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `isMonicOfDegree_two_iff` `neg_neg` `isMonicOfDegree_sub_add_two`
`isMonicOfDegree_zero_iff` 📖	mathematical	—	`IsMonicOfDegree` `Polynomial` `instOne`	—	`eq_one_of_monic_natDegree_zero` `natDegree_one`

Polynomial.IsMonicOfDegree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`Polynomial.natDegree` `Polynomial.IsMonicOfDegree`	`Polynomial` `Polynomial.instAdd`	—	`add_comm` `add_right`
`add_right` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Polynomial.natDegree`	`Polynomial` `Polynomial.instAdd`	—	`subsingleton_or_nontrivial` `Polynomial.isMonicOfDegree_iff` `Polynomial.natDegree_add_le_of_degree_le` `Eq.le` `natDegree_eq` `LT.lt.le` `Polynomial.coeff_add_eq_left_of_lt`
`aeval_add` 📖	mathematical	`Polynomial.IsMonicOfDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.instAdd` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`subsingleton_or_nontrivial` `mul_one` `comp` `one_ne_zero` `Polynomial.isMonicOfDegree_X_add_one`
`aeval_sub` 📖	mathematical	`Polynomial.IsMonicOfDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `aeval_add`
`coeff_eq` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial.coeff`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `eq_or_lt_of_le` `Polynomial.isMonicOfDegree_iff` `LE.le.trans_lt` `Polynomial.coeff_eq_zero_of_natDegree_lt`
`comp` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial.comp`	—	`subsingleton_or_nontrivial` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `natDegree_eq` `Polynomial.isMonicOfDegree_iff` `Polynomial.natDegree_comp_le` `Polynomial.coeff_comp_degree_mul_degree` `leadingCoeff_eq` `one_pow` `one_mul`
`exists_natDegree_lt` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial` `Polynomial.instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.natDegree`	—	`Polynomial.eraseLead_add_C_mul_X_pow` `add_comm` `natDegree_eq` `leadingCoeff_eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `LE.le.trans_lt` `Polynomial.eraseLead_natDegree_le`
`leadingCoeff_eq` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial.leadingCoeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Polynomial.Monic.def` `monic`
`monic` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial.Monic`	—	—
`mul` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial` `Polynomial.instMul`	—	`subsingleton_or_nontrivial` `leadingCoeff_eq` `one_mul` `one_ne_zero` `NeZero.one` `Polynomial.natDegree_mul'` `natDegree_eq` `Polynomial.Monic.mul` `monic`
`natDegree_eq` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial.natDegree`	—	—
`natDegree_sub_X_pow` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Ring.toSemiring`	`Polynomial.natDegree` `Polynomial` `Polynomial.instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X`	—	`exists_natDegree_lt` `add_sub_cancel_left`
`natDegree_sub_lt` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Ring.toSemiring`	`Polynomial.natDegree` `Polynomial` `Polynomial.instSub`	—	`sub_sub_sub_cancel_right` `natDegree_sub_X_pow` `Polynomial.natDegree_sub_le_iff_left`
`ne_zero` 📖	—	`Polynomial.IsMonicOfDegree`	—	—	`Polynomial.Monic.ne_zero` `monic`
`of_dvd_add` 📖	mathematical	`Polynomial.IsMonicOfDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.natDegree` `Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Polynomial.instAdd`	`Polynomial.instSub` `CommRing.toRing` `Polynomial.instMul`	—	`exists_eq_mul_left_of_dvd` `of_mul_right` `add_right` `eq_sub_iff_add_eq`
`of_dvd_sub` 📖	mathematical	`Polynomial.IsMonicOfDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.natDegree` `Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `Polynomial.instSub` `CommRing.toRing`	`Polynomial.instAdd` `Polynomial.instMul`	—	`sub_neg_eq_add` `of_dvd_add` `Polynomial.natDegree_neg`
`of_mul_left` 📖	—	`Polynomial.IsMonicOfDegree` `Polynomial` `Polynomial.instMul`	—	—	`subsingleton_or_nontrivial` `Polynomial.Monic.of_mul_monic_left` `monic` `natDegree_eq` `leadingCoeff_eq` `Polynomial.Monic.leadingCoeff` `one_mul` `one_ne_zero` `NeZero.one` `Polynomial.natDegree_mul'`
`of_mul_right` 📖	—	`Polynomial.IsMonicOfDegree` `Polynomial` `Polynomial.instMul`	—	—	`subsingleton_or_nontrivial` `Polynomial.Monic.of_mul_monic_right` `monic` `natDegree_eq` `Polynomial.Monic.leadingCoeff` `leadingCoeff_eq` `one_mul` `one_ne_zero` `NeZero.one` `Polynomial.natDegree_mul'`
`pow` 📖	mathematical	`Polynomial.IsMonicOfDegree`	`Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	—	`pow_zero` `MulZeroClass.mul_zero` `pow_succ` `mul_add` `Distrib.leftDistribClass` `mul_one` `mul`
`sub` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Ring.toSemiring` `Polynomial.natDegree`	`Polynomial` `Polynomial.instSub`	—	`sub_eq_add_neg` `add_right` `Polynomial.natDegree_neg`

---

← Back to Index