pow_left_inj — Mathlib

English

Let M be a monoid that is torsion-free. For n ≠ 0, and all a,b in M, a^n = b^n if and only if a = b.

Русский

Пусть M — моноид без торсии. Для n ≠ 0 и любых a,b ∈ M выполняется a^n = b^n тогда и только тогда, когда a = b.

LaTeX

$$$$\forall M \,[\mathrm{Monoid}\ M]\,[\mathrm{IsMulTorsionFree}\ M] \forall n \in \mathbb{N},\ n \neq 0 \Rightarrow \forall a,b \in M,\ a^n = b^n \iff a = b.$$$$

Lean4

@[to_additive nsmul_right_inj]
theorem pow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b :=
  (pow_left_injective hn).eq_iff

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