Theorems · Theorem · field theory

Polynomial.irreducible_iff_lt_natDegree_lt

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

To check a polynomial p over a field is irreducible, it suffices to check there are no divisors of degree 0 < d ≤ degree p / 2. See also: Polynomial.Monic.irreducible_iff_natDegree'.

Defined in

Mathlib.Algebra.Polynomial.FieldDivision

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field