Theorems · Theorem · field theory
Polynomial.natDegree_eq_zero_iff_degree_le_zero
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 ↔ p.degree ≤ 0- Defined in
- Mathlib.Algebra.Polynomial.Degree.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Nat.cast_zeroproof · cited by 1,870
- WithBotstatement and proof · cited by 1,498
- Polynomial.natDegreestatement · cited by 1,105
- Polynomial.degreestatement and proof · cited by 643
- nonpos_iff_eq_zeroproof · cited by 100
- Polynomial.natDegree_le_iff_degree_leproof · cited by 12
Cited by12
Results whose statement or proof uses this declaration.
- Polynomial.degree_eq_zero_of_isUnitproof · cited by 14
- Polynomial.natDegree_compproof · cited by 13
- Polynomial.derivative_eq_zeroproof · cited by 4
- Polynomial.Monic.degree_le_zero_iff_eq_oneproof · cited by 3
- Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonnegproof · cited by 3
- Polynomial.exists_separable_of_irreducibleproof · cited by 1
- IsPrimitiveRoot.sum_eq_zero_iff_forall_eqproof · cited by 1
- Polynomial.Gal.prime_degree_dvd_cardproof · cited by 1
- Polynomial.Splits.of_degree_le_zeroproof · cited by 1
- IsAlgClosed.roots_eq_zero_iff_degree_nonposproof · cited by 0
- Polynomial.tendsto_nhds_iffproof · cited by 0
- Polynomial.degree_zero_leproof · cited by 0