Theorems · Theorem · field theory

IntermediateField.normalClosure_mono

∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L]
  (K K' : IntermediateField F L) [Normal F L],
  K ≤ K' → IntermediateField.normalClosure F (↥K) L ≤ IntermediateField.normalClosure F (↥K') L

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraNormal