English
PUnit, with Monoid R, carries a MulDistribMulAction structure; in particular, smul_mul and smul_one hold: r · (x y) = (r · x) (r · y) and r · 1 = 1.
Русский
PUnit, с моноидом R, имеет структуру MulDistribMulAction; в частности, выполняются smul_mul и smul_one: r · (x y) = (r · x) (r · y) и r · 1 = 1.
LaTeX
$$$\\text{smul\\_mul: } r \\cdot (x y) = (r \\cdot x)(r \\cdot y), \\quad \\text{smul\\_one: } r \\cdot 1 = 1.$$$
Lean4
instance mulDistribMulAction [Monoid R] : MulDistribMulAction R PUnit
where
__ := PUnit.mulAction
smul_mul := by subsingleton
smul_one := by subsingleton