infinite_range_add_smul_iff — Mathlib

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

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