Find home for submodule closure lemma

Stream: mathlib4

[Artie Khovanov]

@[to_additive]
theorem Submonoid.closure_eq_image_multiset_prod {M : Type*} [CommMonoid M] (s : Set M) :
    ↑(closure s) = Multiset.prod '' {m : Multiset M | ∀ x ∈ m, x ∈ s} := by
  ext x
  refine ⟨fun h ↦ Submonoid.exists_multiset_of_mem_closure h, fun h ↦ ?_⟩
  rcases h with ⟨m, hm, rfl⟩
  exact Submonoid.multiset_prod_mem _ _ (by aesop)

#find_home Submonoid.closure_eq_image_multiset_prod -- Mathlib.Algebra.Ring.Subsemiring.Basic

It feels like it should live in Algebra.Group.Submonoid.Membership next to docs#Submonoid.exists_multiset_of_mem_closure, but that file doesn't have docs#Submonoid.multiset_prod_mem!

note: this is the "index free" version of the lemma that says that the elements of a submonoid closure of a set are finite products of elements of the set