Theorems · Definition · field theory

IsAlgClosed.lift

{M : Type w} →
  [inst : Field M] →
    [IsAlgClosed M] →
      {R : Type u} →
        [inst_2 : CommRing R] →
          [IsDomain R] →
            {S : Type v} →
              [inst_4 : CommRing S] →
                [IsDomain S] →
                  [inst_6 : Algebra R S] →
                    [inst_7 : Algebra R M] →
                      [Module.IsTorsionFree R S] → [Module.IsTorsionFree R M] → [Algebra.IsAlgebraic R S] → S →ₐ[R] M

A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedCommRingIsDomainCommRingIsDomainAlgebraAlgebraModule.IsTorsionFreeModule.IsTorsionFreeAlgebra.IsAlgebraic