English
Let V be a k-vector space with a compatible G-action coming from the MonoidAlgebra structure. For each g in G, the corresponding GroupSMul linear map acts on v ∈ V by multiplying v with the basis element at g, i.e. (GroupSMul.linearMap k V g)(v) = single(g,1) · v.
Русский
Пусть V --- векторное пространство над k с совместимым действием группы G, порождаемым структурой MonoidAlgebra. Для каждого элемента g ∈ G соответствующая линейная карта GroupSMul действует на v ∈ V так, как умножение на базисный вектор при индексе g: (GroupSMul.linearMap k V g)(v) = single(g,1) · v.
LaTeX
$$$ (\\mathrm{GroupSMul}.linearMap\\ k\\ V\\ g)\\ v \\\\;=\\; \\mathrm{single}(g,1) \\cdot v $$$
Lean4
@[simp]
theorem linearMap_apply [Monoid G] [CommSemiring k] (V : Type*) [AddCommMonoid V] [Module k V]
[Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) :
(GroupSMul.linearMap k V g) v = single g (1 : k) • v :=
rfl
