asGroupHom_apply — Mathlib

English

For a representation ρ, applying the group-hom construction to g yields the invertible linear map ρ(g) on V; i.e. the underlying linear map of the unit corresponding to g is ρ(g).

Русский

Для данного представления ρ применение преобразования в группу приводит к обратимому линейному отображению ρ(g) на V; т.е. линейное отображение, соответствующее g, равно ρ(g).

LaTeX

$$$ ↑(asGroupHom \\ ρ \\, g) = ρ(g) $$$

Lean4

theorem asGroupHom_apply (g : G) : ↑(asGroupHom ρ g) = ρ g := by simp only [asGroupHom, MonoidHom.coe_toHomUnits]

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