Theorems · Theorem · field theory

Polynomial.irreducible_comp

∀ {K : Type u} [inst : Field K] {f g : Polynomial K},
  f.Monic →
    g.Monic →
      Irreducible f →
        (∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
            minpoly K x = f →
              Irreducible
                (Polynomial.map (algebraMap K ↥K⟮x⟯) g - Polynomial.C (IntermediateField.AdjoinSimple.gen K x))) →
          Irreducible (f.comp g)

Let f, g be monic polynomials over K. If f is irreducible, and g(x) - α is irreducible in K⟮α⟯ with α a root of f, then f(g(x)) is irreducible.

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field