zpow_left_inj — Mathlib

English

In a torsion-free group, for n ≠ 0, a^n = b^n if and only if a = b.

Русский

В торсионно свободной группе для n ≠ 0 выполняется a^n = b^n ⇔ a = b.

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

@[to_additive zsmul_right_inj]
theorem zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b :=
  (zpow_left_injective hn).eq_iff

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