span_int_eq_addSubgroupClosure — Mathlib

English

In an additive abelian group M, the span over integers of s equals AddSubgroup.closure s.

Русский

В абелевой группе M линейное порождение по целым числам множества s совпадает с порождённой подпгруппой.

LaTeX

$$$$ (\operatorname{span} \mathbb{Z} s).\text{toAddSubgroup} = \operatorname{AddSubgroup}.closure s $$$$

Lean4

theorem span_int_eq_addSubgroupClosure {M : Type*} [AddCommGroup M] (s : Set M) :
    (span ℤ s).toAddSubgroup = AddSubgroup.closure s :=
  Eq.symm <|
    AddSubgroup.closure_eq_of_le _ subset_span fun _ hx =>
      span_induction (fun _ hx => AddSubgroup.subset_closure hx) (AddSubgroup.zero_mem _)
        (fun _ _ _ _ => AddSubgroup.add_mem _) (fun _ _ _ _ => AddSubgroup.zsmul_mem _ ‹_› _) hx

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