I am still not really convinced that semigroup is worth the trouble, but I'm happy to follow the crowd here, and I don't want to belabor any points made by Norm. I just wanted to remark that if you want to prove that Semigroup C. Monoid, the easiest example (that already exists!) is NN.
On Sun, Feb 2, 2020 at 2:03 PM 'fl' via Metamath <[email protected]> wrote: > > > @benoit and @alexander - Thank you for your comments. Go ahead and import >> semigroup (assuming no one else objects). Hopefully, though, I've >> communicated my point that we don't want this to lead to flurry of shallow >> definitions that people must learn, just to address a perceived difficulty >> in understanding the df-* statements (that are technical definitions not >> always meant to be read directly by humans). >> >> > > I think you have taken the right decision. Your contributors will be > grateful. > > -- > FL > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/751ddf1b-388e-49ce-a32c-ec09d8fdaecd%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/751ddf1b-388e-49ce-a32c-ec09d8fdaecd%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSv-Or%2B5JOsMT4Cpa7xE13rpf4d55yS6bac0Pjs9e%3DxrrA%40mail.gmail.com.
