Theorems · Theorem · field theory
Polynomial.Monic.ne_zero
∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {p : Polynomial R}, p.Monic → p ≠ 0- Defined in
- Mathlib.Algebra.Polynomial.Degree.Defs
- Cited by
- 63 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringNontrivial
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Nontrivialstatement and proof · cited by 2,416
- Polynomial.Monicstatement and proof · cited by 461
Cited by63
Results whose statement or proof uses this declaration.
- minpoly.ne_zeroproof · cited by 44
- minpoly.irreducibleproof · cited by 26
- RatFunc.denom_ne_zeroproof · cited by 20
- IsIntegral.isAlgebraicproof · cited by 18
- Polynomial.modByMonic_eq_zero_iff_dvdproof · cited by 15
- Polynomial.div_modByMonic_uniqueproof · cited by 12
- Polynomial.cyclotomic_ne_zeroproof · cited by 11
- Polynomial.natDegree_divByMonicproof · cited by 5
- minpoly.add_algebraMapproof · cited by 4
- Polynomial.degree_add_divByMonicproof · cited by 4
- Polynomial.int_coeff_of_cyclotomic'proof · cited by 3
- LinearMap.nilRank_le_natTrailingDegree_charpolyproof · cited by 3