Theorems · Definition · field theory

Algebra.IsAlgebraic.algEquivEquivAlgHom

(K : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing K] →
      [IsDomain K] →
        [inst_2 : Field L] →
          [inst_3 : Algebra K L] → [Module.IsTorsionFree K L] → [Algebra.IsAlgebraic K L] → (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Defined in

Mathlib.RingTheory.Algebraic.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFieldAlgebraModule.IsTorsionFreeAlgebra.IsAlgebraic