Theorems · Theorem · field theory

IntermediateField.normal_iff_forall_map_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 ↔ ∀ (σ : L →ₐ[F] L), IntermediateField.map σ K = K

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNormal