Zulip Chat Archive

Stream: maths

Topic: monoid structure on set G


view this post on Zulip 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 }

view this post on Zulip Reid Barton (Nov 29 2020 at 01:03):

Yes, it's in https://leanprover-community.github.io/mathlib_docs/algebra/pointwise.html


Last updated: May 06 2021 at 19:30 UTC