Theorems · Theorem · field theory

Polynomial.IsSplittingField.mul

∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra F K] [inst_5 : Algebra F L] [IsScalarTower F K L] (f g : Polynomial F),
  f ≠ 0 →
    g ≠ 0 →
      ∀ [Polynomial.IsSplittingField F K f] [Polynomial.IsSplittingField K L (Polynomial.map (algebraMap F K) g)],
        Polynomial.IsSplittingField F L (f * g)

Defined in

Mathlib.FieldTheory.SplittingField.IsSplittingField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraAlgebraIsScalarTowerPolynomial.IsSplittingFieldPolynomial.IsSplittingField