English
An element x belongs to the sum span {y} + I if and only if there exist a and b ∈ I with a y + b = x.
Русский
Элемент x принадлежит сумме порожденной {y} и идеалом I тогда и только тогда, когда существуют a и b ∈ I такие, что a y + b = x.
LaTeX
$$$$ x \in \operatorname{span} \{ y \} \sqcup I \iff \exists a \in \alpha, \exists b \in I, a \cdot y + b = x $$$$
Lean4
theorem mem_span_singleton_sup {x y : α} {I : Ideal α} : x ∈ Ideal.span { y } ⊔ I ↔ ∃ a : α, ∃ b ∈ I, a * y + b = x :=
by
rw [Submodule.mem_sup]
constructor
· rintro ⟨ya, hya, b, hb, rfl⟩
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
exact ⟨a, b, hb, rfl⟩
· rintro ⟨a, b, hb, rfl⟩
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩
