instDistribSMulUnits

Mathlib.Algebra.GroupWithZero.Action.Units

URI: https://scilib.ai/kg/mathlib#Units.instDistribSMulUnits

English

There is a Distri but SMul on α by Units M: smul_add m = smul_add (m : M) for units m.

Русский

Существует распределённое действие SMul на α со стороны Units M: smul_add m = smul_add (m : M).

LaTeX

$$$\\text{DistribSMul } (Units\, M) \\; \\alpha$$$

Lean4

instance instDistribSMulUnits [Monoid M] [AddZeroClass α] [DistribSMul M α] : DistribSMul Mˣ α where
  smul_add m := smul_add (m : M)

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

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

Разделы

Аффилиация

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