restrictNormal_trans — Mathlib

English

For a Normal F E and χ an isomorphism, restricting χ to E commutes with algebra maps also restricting to K2, K1.

Русский

При Normal F E и изоморфизме χ ограничение χ на E коммутирует с ограничениями отображений на K2, K1.

LaTeX

$$$\alpha\_{E}^K(χ) = χ\restriction_E \circ α^K$$$

Lean4

theorem restrictNormal_trans [Normal F E] :
    (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E) :=
  AlgEquiv.ext fun _ =>
    (algebraMap E K₃).injective (by simp only [AlgEquiv.trans_apply, AlgEquiv.restrictNormal_commutes])

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