pow_right_injective₀ — Mathlib

English

In a CancelMonoidWithZero M that is IsMulTorsionFree, if x ≠ 1 and x ≠ 0, then n ↦ x^n is injective.

Русский

В CancelMonoidWithZero M, являющемся IsMulTorsionFree, если x ≠ 1 и x ≠ 0, то n ↦ x^n инъективно.

LaTeX

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

Lean4

theorem pow_right_injective₀ {M : Type*} [CancelMonoidWithZero M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1)
    (hx' : x ≠ 0) : Function.Injective (fun n ↦ x ^ n) :=
  IsLeftRegular.pow_injective (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx') hx

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