pow_right_injective — Mathlib

English

Let M be a monoid with IsMulTorsionFree; If x is left regular and x ≠ 1, then n ↦ x^n is injective.

Русский

Пусть M — моноид с IsMulTorsionFree; если x — левый регулярный и x ≠ 1, то n ↦ x^n инъективно.

LaTeX

$$$$\\operatorname{IsLeftRegular}(x) \\land x \\neq 1 \\Rightarrow \\operatorname{Injective}(n \\mapsto x^n)$$$$

Lean4

theorem pow_right_injective {M : Type*} [CancelMonoid M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) :
    Function.Injective (fun n ↦ x ^ n) :=
  IsLeftRegular.pow_injective (IsLeftRegular.all x) hx

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