mulDistribMulAction — Mathlib

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

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