Edit zringmpg comment in set.mm and iset.mm

Change multiplication group to multiplicative group
metamath · Mar 8, 2025 · bea539a · bea539a
1 parent 6d6c718
commit bea539a
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/iset.mm b/iset.mm
@@ -153331,8 +153331,8 @@ According to Wikipedia ("Integer", 25-May-2019,
       PJABCRSDTUA $.
   $}
 
-  $( The multiplication group of the ring of integers is the restriction of the
-     multiplication group of the complex numbers to the integers.  (Contributed
+  $( The multiplicative group of the ring of integers is the restriction of the
+     multiplicative group of the complex numbers to the integers.  (Contributed
      by AV, 15-Jun-2019.) $)
   zringmpg $p |- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring ) $=
     ( ccnfld crg wcel cz cvv cmgp cfv cress co czring wceq cnring df-zring eqid

diff --git a/set.mm b/set.mm
@@ -268471,8 +268471,8 @@ According to Wikipedia ("Integer", 25-May-2019,
       PJABCRSDTUA $.
   $}
 
-  $( The multiplication group of the ring of integers is the restriction of the
-     multiplication group of the complex numbers to the integers.  (Contributed
+  $( The multiplicative group of the ring of integers is the restriction of the
+     multiplicative group of the complex numbers to the integers.  (Contributed
      by AV, 15-Jun-2019.) $)
   zringmpg $p |- ( ( mulGrp ` CCfld ) |`s ZZ ) = ( mulGrp ` ZZring ) $=
     ( ccnfld cdr wcel cz cvv cmgp cfv cress co czring wceq cndrng df-zring eqid