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