Theorems · Theorem · field theory

Normal.of_equiv_equiv

∀ {F : Type u_1} [inst : Field F] {E : Type u_3} [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_5} {N : Type u_6}
  [inst_3 : Field N] [inst_4 : Field M] [inst_5 : Algebra M N] [h : Normal F E] {f : F ≃+* M} {g : E ≃+* N},
  (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E) → Normal M N

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldFieldAlgebraNormal