one — Mathlib

English

In any monoid R acting on M, the unit element 1 of R acts regularly on M; that is, 1 is M-regular.

Русский

В любом моноиде R, действующем на M, единица 1 действует регулярно на M; то есть 1-регулярен на M.

LaTeX

$$$\mathrm{IsSMulRegular}_M(1)\;\text{holds.}$$$

Lean4

/-- One is always `M`-regular. -/
@[simp]
theorem one : IsSMulRegular M (1 : R) := fun a b ab =>
  by
  dsimp only [Function.comp_def] at ab
  rw [one_smul, one_smul] at ab
  assumption

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