English
Let I be an ideal, and m ∈ M. Then x ∈ I · span {m} if and only if there exists y ∈ I with y • m = x.
Русский
Пусть I — идеал, и m ∈ M. Тогда x ∈ I · span {m} тогда и только тогда, когда существует y ∈ I такое, что y • m = x.
LaTeX
$$$x \\in I \\cdot \\operatorname{span} (\\{m\\}) \\iff \\exists y \\in I, y \\cdot m = x$$$
Lean4
theorem mem_smul_span_singleton {I : Ideal R} {m : M} {x : M} : x ∈ I • span R ({ m } : Set M) ↔ ∃ y ∈ I, y • m = x :=
⟨fun hx =>
smul_induction_on hx
(fun r hri _ hnm =>
let ⟨s, hs⟩ := mem_span_singleton.1 hnm
⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩)
fun m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩ => ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩,
fun ⟨_, hyi, hy⟩ => hy ▸ smul_mem_smul hyi (subset_span <| Set.mem_singleton m)⟩
