weightHom_toLinearMap — Mathlib

English

For any g in Aut P, the underlying linear map of weightHom(P,g) is the same as Hom.weightHom(P,g.toHom).

Русский

Для любого g ∈ Aut P соответствующая линейная карта weightHom(P,g) совпадает с Hom.weightHom(P,g.toHom).

LaTeX

$$$\\\\big(\\\\mathrm{weightHom}(P)\\, g\\big)^{\\\\mathrm{toLinearMap}} = \\\\mathrm{Hom.weightHom}(P, g^{toHom}).$$$

Lean4

theorem weightHom_toLinearMap {P : RootPairing ι R M N} (g : Aut P) :
    (weightHom P g).toLinearMap = Hom.weightHom P g.toHom :=
  rfl

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