pow_injective — Mathlib

English

If x is right regular and x ≠ 1 in a monoid, then the map n ↦ x^n is injective.

Русский

Если x — правая регулярность и x ≠ 1 в моноиде, то отображение n ↦ x^n инъективно.

LaTeX

$$$$\\operatorname{IsRightRegular}(x) \\wedge x \\neq 1 \\Rightarrow \\operatorname{Injective}(n \\mapsto x^n)$$$$

Lean4

@[to_additive]
theorem pow_injective {M : Type*} [Monoid M] [IsMulTorsionFree M] {x : M} (hx : IsRightRegular x) (hx' : x ≠ 1) :
    Function.Injective (fun n ↦ x ^ n) :=
  MulOpposite.unop_injective.comp <|
    (isLeftRegular_op.mpr hx).pow_injective <| (MulOpposite.op_eq_one_iff x).not.mpr hx'

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