Theorems · Theorem · field theory
Polynomial.natDegree_pos_iff_degree_pos
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree ↔ 0 < p.degree- Defined in
- Mathlib.Algebra.Polynomial.Degree.Defs
- Cited by
- 22 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.
Cites7
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
- lt_iff_lt_of_le_iff_leproof · cited by 54
- Polynomial.natDegree_le_iff_degree_leproof · cited by 12
Cited by22
Results whose statement or proof uses this declaration.
- minpoly.degree_posproof · cited by 6
- Polynomial.not_isUnit_of_natDegree_posproof · cited by 5
- Polynomial.derivative_eq_zeroproof · cited by 4
- Polynomial.separable_orproof · cited by 3
- Polynomial.tendsto_atTop_of_leadingCoeff_nonnegproof · cited by 3
- X_pow_sub_C_irreducible_of_primeproof · cited by 2
- Irreducible.degree_posproof · cited by 2
- FirstOrder.Field.isAlgClosed_of_model_ACFproof · cited by 2
- Polynomial.sum_derivRootWeight_posproof · cited by 2
- Polynomial.irreducible_of_eisenstein_criterionproof · cited by 1
- Polynomial.Monic.degree_posproof · cited by 1
- IsAlgClosed.eval_surjectiveproof · cited by 1