asModuleEquiv_symm_map_rho — Mathlib

English

For g ∈ G, the action on ρ.asModule under ρ g is transported to MonoidAlgebra.of g via the symmetry map.

Русский

Для элемента g ∈ G действие ρ g на ρ.asModule переносится через симметричное отображение в MonoidAlgebra.of k G g.

LaTeX

$$ρ.asModuleEquiv.symm (ρ g x) = MonoidAlgebra.of k G g • ρ.asModuleEquiv.symm x$$

Lean4

@[simp]
theorem asModuleEquiv_symm_map_rho (g : G) (x : V) :
    ρ.asModuleEquiv.symm (ρ g x) = MonoidAlgebra.of k G g • ρ.asModuleEquiv.symm x :=
  by
  rw [LinearEquiv.symm_apply_eq]
  simp

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