Theorems · Theorem · commutative algebra

Irreducible.exists_dvd_monic_irreducible_of_isIntegral

∀ {K : Type u_6} {L : Type u_7} [inst : CommRing K] [IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L]
  [Algebra.IsIntegral K L] {f : Polynomial L},
  Irreducible f → ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g

If L / K is an integral extension, K is a domain, L is a field, then any irreducible polynomial over L divides some monic irreducible polynomial over K.

Defined in

Mathlib.RingTheory.AdjoinRoot

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFieldAlgebraAlgebra.IsIntegral