smul_ofModule_asModule — Mathlib

English

Smul of MonoidAlgebra acts compatibly with the representation when viewed through asModule and RestrictScalars.

Русский

Скалярное умножение MonoidAlgebra совместимо с действием представления, когда рассматривается через asModule и RestrictScalars.

LaTeX

$$smul_ofModule_asModule : r • m = ...$$

Lean4

theorem smul_ofModule_asModule (r : MonoidAlgebra k G) (m : (ofModule M).asModule) :
    (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (r • m)) =
      r • (RestrictScalars.addEquiv k _ _) ((ofModule M).asModuleEquiv (G := G) m) :=
  by
  dsimp
  simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]

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