English
In an infinite ring R, for any x,y ∈ M (an additive group with Ring action) the range of the map r ↦ x + r·y is infinite if and only if y ≠ 0.
Русский
В бесконечном кольце R отображение r ↦ x + r·y имеет бесконечный образ тогда и только тогда, когда y ≠ 0.
LaTeX
$$$\\{x + r y : r\\in R\\}$ бесконечно по мощности ⇔ y \\neq 0$$$
Lean4
@[simp]
theorem infinite_range_add_smul_iff [AddCommGroup M] [Ring R] [Module R M] [Infinite R] [NoZeroSMulDivisors R M]
(x y : M) : (Set.range <| fun r : R ↦ x + r • 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] at hrs
exact smul_left_injective _ h hrs