of_mul_eq_one — Mathlib

English

If an element a is M-regular, then every power a^n is M-regular for all n ∈ N.

Русский

Если элемент a является M-регулярным, то любая степень a^n является M-регулярной для всех n ∈ N.

LaTeX

$$$\forall n \in \mathbb{N},\ IsSMulRegular M a \Rightarrow IsSMulRegular M (a^n)$$$

Lean4

/-- An element of `R` admitting a left inverse is `M`-regular. -/
theorem of_mul_eq_one (h : a * b = 1) : IsSMulRegular M b :=
  of_mul (a := a) (by rw [h]; exact one M)

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