Theorems · Definition · field theory

Field.embProdEmbOfIsAlgebraic

(F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                [inst_5 : Algebra E K] →
                  [IsScalarTower F E K] → [Algebra.IsAlgebraic E K] → Field.Emb F E × Field.Emb E K ≃ Field.Emb F K

If K / E / F is a field extension tower, such that K / E is algebraic, then there is a non-canonical bijection Field.Emb F E × Field.Emb E K ≃ Field.Emb F K. A corollary of algHomEquivSigma.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTowerAlgebra.IsAlgebraic