Taking a look at how subgroups are defined in set.mm (and submonoids, and I presume other sub-structures), I was surprised by what I found. It seems to be a mapping from a group to a (not necessarily proper) subset of the elements of the group. My (possibly naive) expectation was for SubGrp to be a relation on groups so that "A SubGrp B" means that A is a subgroup of B.
Is there a particular advantage to this definition? Aside: I'm looking at this from the perspective of (hopefully) introducing the concept of Simple Groups to set.mm soon. -- 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/4b6795db-2d9b-48f6-8654-ae7703b85c05%40googlegroups.com.
