The given definition of magma is:
df-mgm |- Mgm = { g | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b
A. y e. b ( x o y ) e. b }
Would it be ok to define magma as follows:
df-mgm |- Mgm = { g | A. x e. ( Base ` g ) A. y e. ( Base ` g ) ( x ( +g
` g ) y ) e. ( Base ` g ) }
If so, what problems would result ?
In other words, why was the given definition chosen over the more explicit
definition ?
--
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/3e26ed0a-5b15-4c29-adf5-434fb591eb96n%40googlegroups.com.
