Description: Define the multiplicative
identity, i.e., the monoid identity (df-0g 12628)
of the multiplicative monoid (df-mgp 12926) of a ring-like structure. This
definition works by transferring the multiplicative operation from the
 slot to the
 slot and then
looking at the element which is
then the 
element, that is an identity with respect to the operation
which started out in the slot.
See also dfur2g 12938, which derives the "traditional"
definition as the
unique element of a ring which is left- and right-neutral under
multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario
Carneiro, 27-Dec-2014.) |
mulGrp
