Theorems · Definition · field theory

Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits

{F : Type u_1} →
  {K : Type u_2} →
    (A : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field A] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F A] →
                [Algebra.IsAlgebraic F K] →
                  (L : Type u_4) →
                    [inst_6 : Field L] →
                      [inst_7 : Algebra F L] →
                        [inst_8 : Algebra L A] →
                          [IsScalarTower F L A] →
                            (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
                              (K →ₐ[F] L) ≃ (K →ₐ[F] A)

All F-embeddings of a field K into another field A factor through any subextension of A/F in which the minimal polynomial of elements of K splits.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraAlgebra.IsAlgebraicFieldAlgebraAlgebraIsScalarTower