injective_zpow_iff_not_isOfFinOrder

English

The function n ↦ x^n is injective on Z iff x has no finite order.

Русский

Функция n ↦ x^n инъективна на Z тогда и только тогда, когда у x нет конечного порядка.

LaTeX

$$(Injective (fun n : Z => x^n)) \leftrightarrow \neg IsOfFinOrder x$$

Lean4

@[to_additive (attr := simp)]
theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x :=
  by
  refine ⟨?_, fun h n m hnm => ?_⟩
  · simp_rw [isOfFinOrder_iff_pow_eq_one]
    rintro h ⟨n, hn, hx⟩
    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
  rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm

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