Theorems · Theorem · field theory

AlgHom.restrictNormal_comp

∀ {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],
  (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldFieldAlgebraAlgebraAlgebraFieldAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerNormal