instSMulCommClass_2

Mathlib.Algebra.Ring.CentroidHom

URI: https://scilib.ai/kg/mathlib#CentroidHom.instSMulCommClass_2

English

The scalar action of α on CentroidHom α commutes with the CentroidHom action: SMulCommClass α (CentroidHom α) α.

Русский

Действие α на CentroidHom α коммутирует с действиемCentroidHom: SMulCommClass α (CentroidHom α) α.

LaTeX

$$$\text{SMulCommClass } α (\mathrm{CentroidHom}(α)) α$$$

Lean4

instance : SMulCommClass α (CentroidHom α) α :=
  SMulCommClass.symm _ _ _

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

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

Разделы

Аффилиация

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