Theorems · Theorem · commutative algebra

Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical

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

A polynomial over an irreducible ring R is irreducible if it is monic and irreducible after mapping into an integral domain S (https://math.stackexchange.com/a/4843432/235999). A generalization to Polynomial.Monic.irreducible_of_irreducible_map.

Defined in

Mathlib.RingTheory.Polynomial.IrreducibleRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsPrimeCommRingIsDomain