Theorems · Definition · field theory

IntermediateField.algHomAdjoinIntegralEquiv

(F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {α : E} →
            {K : Type u} →
              [inst_3 : Field K] →
                [inst_4 : Algebra F K] → IsIntegral F α → (↥F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K }

Algebra homomorphism F⟮α⟯ →ₐ[F] K are in bijection with the set of roots of minpoly α in K.

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra