@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).
Norm On Sunday, February 2, 2020 at 11:11:27 AM UTC-5, Alexander van der Vekens wrote: > > I want to comment on the following post in more detail: > > .... -- 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/d61874d9-7a73-4aa5-bbd5-f3a2280585f6%40googlegroups.com.
