Theorems · Theorem · field theory

IntermediateField.normal_iff_forall_fieldRange_eq

∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange = K

If L/K/F is a field tower where L/F is normal, then K is normal over F if and only if σ(K) = K for every σ ∈ K →ₐ[F] L.

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNormal