English
For a nonunital ring R, z ∈ span s iff z ∈ AddSubgroup.closure (univ * s * univ).
Русский
Для небезызначенного кольца R: z ∈ span s тогда и только тогда, когда z ∈ AddSubgroup.closure (univ * s * univ).
LaTeX
$$$ z \\in \\operatorname{span}(s) \\iff z \\in \\operatorname{AddSubgroup.closure} (\\mathrm{univ} * s * \\mathrm{univ})$$$
Lean4
theorem mem_span_iff_mem_addSubgroup_closure {s : Set R} {z : R} :
z ∈ span s ↔ z ∈ AddSubgroup.closure (univ * s * univ) :=
by
trans z ∈ span (univ * s * univ)
· refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
· exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩
· exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _
· refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
· intro x y hy
rw [mul_assoc] at hy ⊢
obtain ⟨r, -, y, hy, rfl⟩ := hy
exact ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
· rintro - x ⟨y, hy, r, -, rfl⟩
exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
