pow_left_injective — Mathlib

English

Let M be a monoid that is torsion-free with respect to multiplication. For every natural number n ≠ 0, the map a ↦ a^n is injective on M.

Русский

Пусть M — моноид, не имеющий торсионности по умножению. Для каждого натурального n ≠ 0 отображение a ↦ a^n на M инъективно.

LaTeX

$$$$\forall M \,[\mathrm{Monoid}\ M]\,[\mathrm{IsMulTorsionFree}\ M],\ \forall n \in \mathbb{N},\ n \neq 0 \Rightarrow \mathrm{Injective}(a \mapsto a^n).$$$$

Lean4

@[to_additive nsmul_right_injective]
theorem pow_left_injective (hn : n ≠ 0) : Injective fun a : M ↦ a ^ n :=
  IsMulTorsionFree.pow_left_injective hn

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