single_smul — Mathlib

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

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