Subgroup vs submodule

Stream: Is there code for X?

[Patrick Massot]

Last question for today:

import Mathlib.LinearAlgebra.Span
import Mathlib.GroupTheory.Subgroup.Basic

example {G : Type*} [AddCommGroup G] {A : Set G} :
    (AddSubgroup.closure A : Set G) = (Submodule.span ℤ A) := by
  sorry

[Timo Carlin-Burns]

Is this what you're looking for? docs#Submodule.span_int_eq_addSubgroup_closure

[Timo Carlin-Burns]

import Mathlib.LinearAlgebra.Span
import Mathlib.GroupTheory.Subgroup.Basic

example {G : Type*} [AddCommGroup G] {A : Set G} :
    (AddSubgroup.closure A : Set G) = (Submodule.span ℤ A) := by
  rw [← Submodule.coe_toAddSubgroup, Submodule.span_int_eq_addSubgroup_closure]

[Patrick Massot]

Perfect, thanks!