restrictNormal_comp — Mathlib

English

Restricting first along K1→K2 and then along K2→K3 yields the same as restricting directly along K1→K3.

Русский

Ограничение последовательно через K1→K2 и затем K2→K3 даёт тот же результат, что и ограничение через K1→K3 напрямую.

LaTeX

$$$\text{restrictNormalHom } K_1 \.f = (\text{restrictNormalHom } K_1)\circ (\text{restrictNormalHom } (F:=F)(K_1:=K_3)K_2)$$$$

Lean4

theorem restrictNormal_comp [Normal F E] :
    (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E :=
  AlgHom.ext fun _ => (algebraMap E K₃).injective (by simp only [AlgHom.comp_apply, AlgHom.restrictNormal_commutes])

Похожие утверждения