English
The left-injectivity of z-powers is equivalent to equality: a^n = b^n iff a = b, for n ≠ 0.
Русский
Левая инъективность z-показателя эквивалентна равенству: a^n = b^n ⇔ a = b, для n ≠ 0.
LaTeX
$$$$\forall G \,[\mathrm{Group } G] \,[\mathrm{IsMulTorsionFree } G] \forall n \in \mathbb{Z},\ n \neq 0 \Rightarrow (a^n = b^n \iff a = b).$$$$
Lean4
/-- Alias of `zpow_left_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'` and
`zsmul_lt_zsmul_iff'`. -/
@[to_additive /-- Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'`
and `zsmul_lt_zsmul_iff'`. -/
]
theorem zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b :=
zpow_left_inj hn
