Theorems · Definition · field theory

IntermediateField.equivMap

{F : Type u_4} →
  [inst : Field F] →
    {E : Type u_5} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type u_6} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] →
                (L : IntermediateField F E) → (f : E →ₐ[F] K) → ↥L ≃ₐ[F] ↥(IntermediateField.map f L)

An intermediate field is isomorphic to its image under an AlgHom (which is automatically injective).

Defined in

Mathlib.FieldTheory.IntermediateField.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra