## Stream: maths

### Topic: monoid structure on set G

#### Thomas Browning (Nov 29 2020 at 00:56):

Does mathlib have this monoid struture on subsets of a monoid? If not, should I PR it?

variables {M : Type*} [monoid M]

instance : monoid (set M) :=
{ one := {1},
mul := λ S T g, ∃ s ∈ S, ∃ t ∈ T, g = s * t,
one_mul := begin
intro S,
ext g,
split,
{ rintro ⟨t, ht, s, hs, hg⟩,
rwa [hg, set.mem_singleton_iff.mp ht, one_mul] },
{ exact λ hg, ⟨1, set.mem_singleton 1, g, hg, (one_mul g).symm⟩ },
end,
mul_one := begin
intro S,
ext g,
split,
{ rintro ⟨t, ht, s, hs, hg⟩,
rwa [hg, set.mem_singleton_iff.mp hs, mul_one] },
{ exact λ hg, ⟨g, hg, 1, set.mem_singleton 1, (mul_one g).symm⟩ },
end,
mul_assoc := begin
intros S T U,
ext g,
split,
{ rintros ⟨st, ⟨s, hs, t, ht, hst⟩, u, hu, hg⟩,
exact ⟨s, hs, t * u, ⟨t, ht, u, hu, rfl⟩, by rw [hg, hst, mul_assoc]⟩ },
{ rintros ⟨s, hs, tu, ⟨t, ht, u, hu, htu⟩, hg⟩,
exact ⟨s * t, ⟨s, hs, t, ht, rfl⟩, u, hu, by rw [hg, htu, mul_assoc]⟩ },
end }


#### Reid Barton (Nov 29 2020 at 01:03):

Last updated: May 06 2021 at 19:30 UTC