Theorems · Theorem · field theory

Polynomial.Monic.irreducible_iff_lt_natDegree_lt

∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic →
    p ≠ 1 → (Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p)

Alternate phrasing of Polynomial.Monic.irreducible_iff_natDegree' where we only have to check one divisor at a time.

Defined in

Mathlib.Algebra.Polynomial.Monic

Cited by

3 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNoZeroDivisors