Theorems · Definition · field theory

IsSepClosed.lift

{K : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : Field M] → [inst_4 : Algebra K M] → [IsSepClosed M] → [Algebra.IsSeparable K L] → L →ₐ[K] M

A (random) homomorphism from a separable extension L of K into a separably closed extension M of K.

Defined in

Mathlib.FieldTheory.IsSepClosed

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraIsSepClosedAlgebra.IsSeparable