pow_right_inj₀ — Mathlib

English

In a CancelMonoidWithZero M that is IsMulTorsionFree, if x ≠ 1 and x ≠ 0, then x^n = x^m iff n = m.

Русский

В CancelMonoidWithZero M, IsMulTorsionFree, если x ≠ 1 и x ≠ 0, то x^n = x^m эквивалентно n = m.

LaTeX

$$$$\\bigl(x \\neq 1 \\bigr) \\land \\bigl(x \\neq 0\\bigr) \\Rightarrow (x^n = x^m \\iff n = m)$$$$

Lean4

@[simp]
theorem pow_right_inj₀ {M : Type*} [CancelMonoidWithZero M] [IsMulTorsionFree M] {x : M} (hx : x ≠ 1) (hx' : x ≠ 0)
    {n m : ℕ} : x ^ n = x ^ m ↔ n = m :=
  (pow_right_injective₀ hx hx').eq_iff

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