asModuleEquiv_symm_map_smul — Mathlib

English

The symmetric map respects scalar multiplication by elements of k via the algebra map.

Русский

Симметричное отображение сохраняет умножение на скаляры из k посредством алгебраического отображения.

LaTeX

$$ρ.asModuleEquiv.symm (r • x) = algebraMap k (MonoidAlgebra k G) r • ρ.asModuleEquiv.symm x$$

Lean4

theorem asModuleEquiv_symm_map_smul (r : k) (x : V) :
    ρ.asModuleEquiv.symm (r • x) = algebraMap k (MonoidAlgebra k G) r • ρ.asModuleEquiv.symm x :=
  by
  rw [LinearEquiv.symm_apply_eq]
  simp

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