asModuleEquiv_map_smul — Mathlib

English

For any r in MonoidAlgebra k G and x in ρ.asModule, the module equivalence carries the action compatibly with the algebra action.

Русский

Для любого r в MonoidAlgebra k G и x в ρ.asModule, отображение эквивалентности модуля совместимо с действием алгебры.

LaTeX

$$ρ.asModuleEquiv (r • x) = ρ.asAlgebraHom r (ρ.asModuleEquiv x)$$

Lean4

@[simp]
theorem asModuleEquiv_map_smul (r : MonoidAlgebra k G) (x : ρ.asModule) :
    ρ.asModuleEquiv (r • x) = ρ.asAlgebraHom r (ρ.asModuleEquiv x) :=
  rfl

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