mk'_smul

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalizedModule.mk'_smul

English

The mk' operation is compatible with scalar multiplication: mk' f (r·m) s = r·mk' f m s.

Русский

Операция mk' совместима с умножением на скаляры: mk' f (r·m) s = r·mk' f m s.

LaTeX

$$$mk' f (r\\cdot m) s = r\\cdot mk' f m s$$$

Lean4

theorem mk'_smul (r : R) (m : M) (s : S) : mk' f (r • m) s = r • mk' f m s :=
  by
  delta mk'
  rw [← LocalizedModule.smul'_mk, LinearMap.map_smul]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru