Theorems · Theorem · field theory

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

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNormal