Theorems · Theorem · field theory

AlgEquiv.restrictNormal_commutes

∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
  [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E] (x : E),
  (algebraMap E K₂) ((χ.restrictNormal E) x) = χ ((algebraMap E K₁) x)

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

13 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal