infinite_range_add_nsmul_iff — Mathlib

English

For an additive group M with NoZeroSmulDivisors by ℤ, the range of x + n·y over n ∈ ℕ is infinite iff y ≠ 0.

Русский

Для аддитивной группы M с NoZeroSmulDivisors по ℤ образ {x + n y : n ∈ ℕ} бесконечен тогда и только тогда, когда y ≠ 0.

LaTeX

$$$\\{x + n y : n \\in \\mathbb{N}\\}$ бесконечно ⇔ y \\neq 0$$$

Lean4

@[simp]
theorem infinite_range_add_nsmul_iff [AddCommGroup M] [NoZeroSMulDivisors ℤ M] (x y : M) :
    (Set.range <| fun n : ℕ ↦ x + n • y).Infinite ↔ y ≠ 0 :=
  by
  refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩
  rw [add_right_inj, ← natCast_zsmul, ← natCast_zsmul] at hrs
  simpa using smul_left_injective _ h hrs

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