English
In an additive abelian group M, the span over integers of a set s coincides with the subgroup generated by s.
Русский
В абелевой группе M линейное порождение по целым числам множества s совпадает с порождённой подпгруппой,/generated by s.
LaTeX
$$$$(\\operatorname{span} \\mathbb{Z} s).\\text{toAddSubgroup} = \\operatorname{AddSubgroup}.closure\, s$$$$
Lean4
/-- A variant of `span_induction` that combines `∀ x ∈ s, p x` and `∀ r x, p x → p (r • x)`
into a single condition `∀ r, ∀ x ∈ s, p (r • x)`, which can be easier to verify. -/
@[elab_as_elim]
theorem closure_induction {p : (x : M) → x ∈ span R s → Prop} (zero : p 0 (Submodule.zero_mem _))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
(smul_mem : ∀ (r x) (h : x ∈ s), p (r • x) (Submodule.smul_mem _ _ <| subset_span h)) {x} (hx : x ∈ span R s) :
p x hx := by
have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]
refine
AddSubmonoid.closure_induction (motive := fun x hx ↦ p x (key.mpr hx)) ?_ zero (by simpa only [key] using add)
(key.mp hx)
rintro - ⟨r, -, x, hx, rfl⟩
exact smul_mem r x hx
