smul_isUnit — Mathlib

English

If m is a unit of M, then its action on a equals the action of the underlying monoid element.

Русский

Если m является элементом-единицей M, то действие m на a равно действию его основания.

LaTeX

$$$ [Monoid M] [SMul M \\alpha] {m\\in M^×} \\; (smul\\_isUnit) : m^\\text{unit} \\cdot a = m \\cdot a $$$

Lean4

@[simp]
theorem smul_isUnit [Monoid M] [SMul M α] {m : M} (hm : IsUnit m) (a : α) : hm.unit • a = m • a :=
  rfl

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