nat_smulCommClass'

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#AddMonoid.nat_smulCommClass'

English

Symmetric variant: SMulCommClass M Nat A, asserting the same commutativity with Nat and M when acting on A.

Русский

Симметричный вариант: SMulCommClass M Nat A, утверждающий ту же commutativity между Nat и M, действующими на A.

LaTeX

$$$\\text{SMulCommClass } M \\mathbb{N} A$$$

Lean4

instance nat_smulCommClass' {M A : Type*} [AddMonoid A] [DistribSMul M A] : SMulCommClass M ℕ A :=
  .symm _ _ _

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

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

Разделы

Аффилиация

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