distribMulAction — Mathlib

English

PUnit, under a Monoid R, forms a DistribMulAction; in particular, smul distributes over zero and addition: r · 0 = 0 and r · (x + y) = r · x + r · y.

Русский

PUnit вместе с моноидом R образует распределимое действие умножения; в частности, скалярное умножение распределимо по нулю и по сумме: r · 0 = 0 и r · (x + y) = r · x + r · y.

LaTeX

$$$\\text{smul\_zero: } r \\cdot 0 = 0, \\quad \\text{smul\_add: } r \\cdot (x+y) = (r\\cdot x) + (r\\cdot y).$$$

Lean4

instance distribMulAction [Monoid R] : DistribMulAction R PUnit
    where
  __ := PUnit.mulAction
  smul_zero := by subsingleton
  smul_add := by subsingleton

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