Theorems · Theorem · field theory

AlgEquiv.restrictNormal_trans

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

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldFieldAlgebraAlgebraAlgebraFieldAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerNormal