SmallDegree

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

Statistics

Metric	Count
Definitions	0
Theorems `eq_X_add_C`, `degree_cubic`, `degree_cubic_le`, `degree_cubic_lt`, `degree_linear`, `degree_linear_le`, `degree_linear_lt`, `degree_linear_lt_degree_C_mul_X_sq`, `degree_quadratic`, `degree_quadratic_le`, `degree_quadratic_lt`, `degree_quadratic_lt_degree_C_mul_X_cb`, `eq_X_add_C_of_degree_eq_one`, `eq_X_add_C_of_degree_le_one`, `eq_X_add_C_of_natDegree_le_one`, `exists_eq_X_add_C_of_natDegree_le_one`, `le_natDegree_of_coe_le_degree`, `leadingCoeff_cubic`, `leadingCoeff_linear`, `leadingCoeff_quadratic`, `natDegree_cubic`, `natDegree_cubic_le`, `natDegree_linear`, `natDegree_linear_le`, `natDegree_quadratic`, `natDegree_quadratic_le`, `ne_zero_of_coe_le_degree`, `zero_le_degree_iff`	28
Total	28

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_cubic` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `WithBot` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_assoc` `degree_add_eq_left_of_degree_lt` `degree_quadratic_lt_degree_C_mul_X_cb` `degree_C_mul_X_pow`
`degree_cubic_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_assoc` `degree_add_le_of_degree_le` `degree_C_mul_X_pow_le` `le_trans` `degree_quadratic_le` `WithBot.coe_le_coe`
`degree_cubic_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`LE.le.trans_lt` `Nat.instAtLeastTwoHAddOfNat` `degree_cubic_le` `WithBot.coe_lt_coe` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`degree_linear` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `WithBot` `WithBot.one` `Nat.instOne`	—	`degree_add_eq_left_of_degree_lt` `degree_C_lt_degree_C_mul_X` `degree_C_mul_X`
`degree_linear_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `WithBot.one` `Nat.instOne`	—	`degree_add_le_of_degree_le` `degree_C_mul_X_le` `le_trans` `degree_C_le` `Nat.WithBot.coe_nonneg`
`degree_linear_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`LE.le.trans_lt` `Nat.instAtLeastTwoHAddOfNat` `degree_linear_le` `WithBot.coe_lt_coe` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`degree_linear_lt_degree_C_mul_X_sq` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`degree_C_mul_X_pow` `degree_linear_lt`
`degree_quadratic` 📖	mathematical	—	`degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `WithBot` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_assoc` `degree_add_eq_left_of_degree_lt` `degree_linear_lt_degree_C_mul_X_sq` `degree_C_mul_X_pow`
`degree_quadratic_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_assoc` `degree_add_le_of_degree_le` `degree_C_mul_X_pow_le` `le_trans` `degree_linear_le` `WithBot.coe_le_coe` `one_le_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`degree_quadratic_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`LE.le.trans_lt` `Nat.instAtLeastTwoHAddOfNat` `degree_quadratic_le` `WithBot.coe_lt_coe` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`degree_quadratic_lt_degree_C_mul_X_cb` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`degree_C_mul_X_pow` `degree_quadratic_lt`
`eq_X_add_C_of_degree_eq_one` 📖	mathematical	`degree` `WithBot` `WithBot.one` `Nat.instOne`	`Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `leadingCoeff` `X` `coeff`	—	`eq_X_add_C_of_degree_le_one` `Eq.le` `leadingCoeff.eq_1` `natDegree_eq_of_degree_eq_some` `Nat.cast_one`
`eq_X_add_C_of_degree_le_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `WithBot.one` `Nat.instOne`	`Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff` `X`	—	`ext` `coeff_add` `mul_coeff_zero` `coeff_C_zero` `coeff_X_zero` `MulZeroClass.mul_zero` `zero_add` `coeff_mul_X` `coeff_C` `coeff_C_succ` `add_zero` `lt_of_le_of_lt` `Nat.one_lt_ofNat` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `coeff_eq_zero_of_degree_lt`
`eq_X_add_C_of_natDegree_le_one` 📖	mathematical	`natDegree`	`Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff` `X`	—	`eq_X_add_C_of_degree_le_one` `degree_le_of_natDegree_le`
`exists_eq_X_add_C_of_natDegree_le_one` 📖	mathematical	`natDegree`	`Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X`	—	`eq_X_add_C_of_natDegree_le_one`
`le_natDegree_of_coe_le_degree` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `degree`	`natDegree`	—	`WithBot.coe_le_coe` `degree_eq_natDegree` `ne_zero_of_coe_le_degree`
`leadingCoeff_cubic` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`add_assoc` `add_comm` `leadingCoeff_add_of_degree_lt` `degree_quadratic_lt_degree_C_mul_X_cb` `leadingCoeff_C_mul_X_pow`
`leadingCoeff_linear` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X`	—	`add_comm` `leadingCoeff_add_of_degree_lt` `degree_C_lt_degree_C_mul_X` `leadingCoeff_C_mul_X`
`leadingCoeff_quadratic` 📖	mathematical	—	`leadingCoeff` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`add_assoc` `add_comm` `leadingCoeff_add_of_degree_lt` `degree_linear_lt_degree_C_mul_X_sq` `leadingCoeff_C_mul_X_pow`
`natDegree_cubic` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`natDegree_eq_of_degree_eq_some` `degree_cubic`
`natDegree_cubic_le` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`natDegree_le_of_degree_le` `degree_cubic_le`
`natDegree_linear` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X`	—	`natDegree_add_C` `natDegree_C_mul_X`
`natDegree_linear_le` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X`	—	`natDegree_le_of_degree_le` `degree_linear_le`
`natDegree_quadratic` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`natDegree_eq_of_degree_eq_some` `degree_quadratic`
`natDegree_quadratic_le` 📖	mathematical	—	`natDegree` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`natDegree_le_of_degree_le` `degree_quadratic_le`
`ne_zero_of_coe_le_degree` 📖	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `degree`	—	—	`zero_le_degree_iff` `LE.le.trans` `WithBot.coe_le_coe`
`zero_le_degree_iff` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree`	—	`not_lt` `Nat.WithBot.lt_zero_iff` `degree_eq_bot`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_X_add_C` 📖	mathematical	`Polynomial.Monic` `Polynomial.natDegree`	`Polynomial` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`one_mul` `Polynomial.C_1` `coeff_natDegree` `Polynomial.eq_X_add_C_of_natDegree_le_one` `Eq.le`

---

← Back to Index