mulAction — Mathlib

English

There exists a natural action of any monoid R on the one-point type PUnit, given by the unique action, and the action satisfies the unit and associativity axioms.

Русский

Существует естественное действие любого моноида R на единичном типе PUnit, заданное единственным действием, удовлетворяющее единичному и ассоциативному законам действия.

LaTeX

$$$(r_1 r_2) \\cdot * = r_1 \\cdot (r_2 \\cdot *) \\quad\\text{and}\\quad 1 \\cdot * = *.$$$

Lean4

instance mulAction [Monoid R] : MulAction R PUnit
    where
  __ := PUnit.smul
  one_smul := by subsingleton
  mul_smul := by subsingleton

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