Theorems · Theorem · field theory

Polynomial.Monic.irreducible_of_irreducible_map

∀ {R : Type u} {S : Type v} [inst : CommRing R] [IsDomain R] [inst_2 : CommRing S] [IsDomain S] (φ : R →+* S)
  (f : Polynomial R), f.Monic → Irreducible (Polynomial.map φ f) → Irreducible f

A polynomial over an integral domain R is irreducible if it is monic and irreducible after mapping into an integral domain S. A special case of this lemma is that a polynomial over ℤ is irreducible if it is monic and irreducible over ℤ/pℤ for some prime p.

Defined in

Mathlib.Algebra.Polynomial.Eval.Irreducible

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomain