of_smul_eq_one — Mathlib

English

An element a acting on s with a left inverse (a • s = 1) is M-regular.

Русский

Элемент a, действующий на s слева как обратная (a • s = 1), является M-регулярным.

LaTeX

$$$a \cdot s = 1 \Rightarrow IsSMulRegular M s$$$

Lean4

/-- An element of `S` admitting a left inverse in `R` is `M`-regular. -/
theorem of_smul_eq_one (h : a • s = 1) : IsSMulRegular M s :=
  of_smul a
    (by
      rw [h]
      exact one M)

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