mkOfSMul_smul

Mathlib.Algebra.Category.ModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.mkOfSMul_smul

English

The scalar action on the mkOfSMul φ module is exactly the endomorphism φ(r): for any r ∈ R, the action of r on the module equals φ(r).

Русский

Действие скаляра на модуле mkOfSMul φ совпадает с φ(r).

LaTeX

$$$\forall r\in R:\; (\mathrm{mkOfSMul}(\phi)).\mathrm{smul}(r) = \phi(r).$$$

Lean4

theorem mkOfSMul_smul (r : R) : (mkOfSMul φ).smul r = φ r :=
  rfl

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

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

Разделы

Аффилиация

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