English
In a k-linear representation ρ of a group G on a k-module V, the basis element δ_g of the Monoid Algebra, scaled by t ∈ k, acts on v ∈ V by t times applying ρ(g) to v.
Русский
В k-линейном представлении ρ группы G на модуле V базисный элемент δ_g моноидной алгебры, умноженный на t ∈ k, действует на v ∈ V как t·(ρ(g) v).
LaTeX
$$$(\\delta_g t) \\cdot v = t \\cdot (\\rho(g) v)$$$
Lean4
@[simp]
theorem single_smul (t : k) (g : G) (v : ρ.asModule) :
MonoidAlgebra.single (g : G) t • v = t • ρ g (ρ.asModuleEquiv v) :=
by
rw [← LinearMap.smul_apply, ← asAlgebraHom_single, ← asModuleEquiv_map_smul]
rfl