injective_pow_iff_not_isOfFinOrder

English

Injectivity of n ↦ x^n is equivalent to x not having finite order.

Русский

Инъективность n ↦ x^n эквивалентна тому, что порядок x бесконечен.

LaTeX

$$Injective (n ↦ x^n) ⇔ ¬IsOfFinOrder(x)$$

Lean4

@[to_additive (attr := simp)]
theorem injective_pow_iff_not_isOfFinOrder : Injective (fun n : ℕ ↦ x ^ n) ↔ ¬IsOfFinOrder x :=
  by
  refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
  rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm

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