Theorems · Theorem · field theory
Polynomial.degree_le_of_natDegree_le
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n → p.degree ≤ ↑nAlias of the forward direction of Polynomial.natDegree_le_iff_degree_le.
- Defined in
- Mathlib.Algebra.Polynomial.Degree.Defs
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement and proof · cited by 5,681
- WithBotstatement · cited by 1,498
- Polynomial.natDegreestatement · cited by 1,105
- Polynomial.degreestatement · cited by 643
- Polynomial.natDegree_le_iff_degree_leproof · cited by 12
Cited by10
Results whose statement or proof uses this declaration.
- Polynomial.eq_C_of_natDegree_le_zeroproof · cited by 6
- Polynomial.eq_X_add_C_of_natDegree_le_oneproof · cited by 2
- IsAdjoinRootMonic.coeff_apply_leproof · cited by 1
- Polynomial.Splits.degree_le_one_of_irreducibleproof · cited by 1
- Polynomial.MonicDegreeEq.degreeproof · cited by 0
- Polynomial.degree_natCast_leproof · cited by 0
- Polynomial.roots_eq_of_natDegree_le_card_of_ne_zeroproof · cited by 0
- Polynomial.Splits.splitsproof · cited by 0
- minpoly.degree_leproof · cited by 0
- Polynomial.degree_intCast_leproof · cited by 0