nat_smulCommClass — Mathlib

English

If A is an AddMonoid and M acts on A distributively, then natural numbers commute with M-action: SMulCommClass Nat M A with nsmul on A.

Русский

Если A — аддитивный монод, и M действует на A распределенно, то натуральные числа коммютируют с действием M: SMulCommClass Nat M A.

LaTeX

$$$\\text{SMulCommClass Nat M A}$$$

Lean4

instance nat_smulCommClass {M A : Type*} [AddMonoid A] [DistribSMul M A] : SMulCommClass ℕ M A where
  smul_comm n x y := ((DistribSMul.toAddMonoidHom A x).map_nsmul y n).symm

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