int_smulCommClass' — Mathlib

English

The symmetric integer action yields a SMulCommClass between M and ℤ on A, i.e. the M-action commutes with integer scaling.

Русский

Симметричная целочисленная операция дает SMulCommClass между M и ℤ на A, то есть действие M коммутивно по отношению к умножению на целые.

LaTeX

$$$\mathrm{SMulCommClass}\ M \mathbb{Z} A$$$

Lean4

instance int_smulCommClass' : SMulCommClass M ℤ A :=
  SMulCommClass.symm _ _ _

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