From c7f3e5c6ac32698e53bee72144df3783cfabb5fa Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 11 Nov 2021 19:35:41 +0000 Subject: [PATCH] feat(group_theory/submonoid/membership): `exists_multiset_of_mem_closure` (#10256) Version of `exists_list_of_mem_closure` for `comm_monoid`. --- src/group_theory/submonoid/membership.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean index 77939521078e8..92c94d4d69e32 100644 --- a/src/group_theory/submonoid/membership.lean +++ b/src/group_theory/submonoid/membership.lean @@ -196,6 +196,14 @@ begin exact ⟨list.map coe l, λ y hy, let ⟨z, hz, hy⟩ := list.mem_map.1 hy in hy ▸ z.2, hx⟩ end +@[to_additive] +lemma exists_multiset_of_mem_closure {M : Type*} [comm_monoid M] {s : set M} + {x : M} (hx : x ∈ closure s) : ∃ (l : multiset M) (hl : ∀ y ∈ l, y ∈ s), l.prod = x := +begin + obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx, + exact ⟨l, h1, (multiset.coe_prod l).trans h2⟩, +end + /-- The submonoid generated by an element. -/ def powers (n : M) : submonoid M := submonoid.copy (powers_hom M n).mrange (set.range ((^) n : ℕ → M)) $