English
Let G be a group that is IsMulTorsionFree. For any nonzero integer n, the map a ↦ a^n is injective.
Русский
Пусть G — группа, торсионно свободная. Для любого ненулевого целого n отображение a ↦ a^n инъективно.
LaTeX
$$$$\forall G \,[\text{Group }G] \,[\mathrm{IsMulTorsionFree } G] \forall n \in \mathbb{Z},\ n \neq 0 \Rightarrow \mathrm{Injective}(a \mapsto a^n).$$$$
Lean4
@[to_additive zsmul_right_injective]
theorem zpow_left_injective : ∀ {n : ℤ}, n ≠ 0 → Injective fun a : G ↦ a ^ n
| (n + 1 : ℕ), _ => by simpa [← Int.natCast_one, ← Int.natCast_add] using pow_left_injective n.succ_ne_zero
| .negSucc n, _ => by simpa using inv_injective.comp (pow_left_injective n.succ_ne_zero)
