Theorems · Theorem · field theory

IntermediateField.algHomEquivAlgHomOfSplits_apply_apply

∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [inst_5 : Algebra.IsAlgebraic F K] (L : IntermediateField F A)
  (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] ↥L) (x : K),
  ((IntermediateField.algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap (↥L) A) (f x)

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraAlgebra.IsAlgebraic