multiplicative neutral element -> unity element

and "neutral element" -> "zero element" (in the context of rings)
avekens · Jan 18, 2025 · 3396ff3 · 3396ff3
1 parent f69068c
commit 3396ff3
Showing 1 changed file with 20 additions and 21 deletions.
diff --git a/set.mm b/set.mm
@@ -256090,7 +256090,7 @@ nonzero elements form a group under multiplication (from which it
   ${
     $d R s $.
     primefld0cl.1 $e |- .0. = ( 0g ` R ) $.
-    $( The prime field contains the neutral element of the division ring.
+    $( The prime field contains the zero element of the division ring.
        (Contributed by Thierry Arnoux, 22-Aug-2023.) $)
     primefld0cl $p |- ( R e. DivRing -> .0. e. |^| ( SubDRing ` R ) ) $=
       ( vs cdr wcel csdrg cfv csubg wss c0 wne cv wi csubrg cress co issdrg syl
@@ -256102,8 +256102,8 @@ nonzero elements form a group under multiplication (from which it
   ${
     $d R s $.
     primefld1cl.1 $e |- .1. = ( 1r ` R ) $.
-    $( The prime field contains the multiplicative neutral element of the
-       division ring.  (Contributed by Thierry Arnoux, 22-Aug-2023.) $)
+    $( The prime field contains the unity element of the division ring.
+       (Contributed by Thierry Arnoux, 22-Aug-2023.) $)
     primefld1cl $p |- ( R e. DivRing -> .1. e. |^| ( SubDRing ` R ) ) $=
       ( vs cdr wcel csdrg cfv cint csubrg wss c0 wne cv wi cress issdrg simp2bi
       co a1i ssrdv cbs eqid sdrgid ne0d subrgint syl2anc subrg1cl syl ) AEFZAGH
@@ -265360,15 +265360,15 @@ According to Wikipedia ("Integer", 25-May-2019,
     ( cvv wcel cmul czring cmulr cfv wceq zex ccnfld df-zring cnfldmul ressmulr
     cz ax-mp ) MABCDEFGHMIDCAJKLN $.
 
-  $( The neutral element of the ring of integers.  (Contributed by Thierry
-     Arnoux, 1-Nov-2017.)  (Revised by AV, 9-Jun-2019.) $)
+  $( The zero element of the ring of integers.  (Contributed by Thierry Arnoux,
+     1-Nov-2017.)  (Revised by AV, 9-Jun-2019.) $)
   zring0 $p |- 0 = ( 0g ` ZZring ) $=
     ( ccnfld cmnd wcel cc0 cz wss czring c0g cfv wceq ccrg crg crngring ringmnd
     cc cncrng mp2b 0z zsscn df-zring cnfldbas cnfld0 ress0g mp3an ) ABCZDECEOFD
     GHIJAKCALCUEPAMANQRSEOAGDTUAUBUCUD $.
 
-  $( The multiplicative neutral element of the ring of integers.  (Contributed
-     by Thierry Arnoux, 1-Nov-2017.)  (Revised by AV, 9-Jun-2019.) $)
+  $( The unity element of the ring of integers.  (Contributed by Thierry
+     Arnoux, 1-Nov-2017.)  (Revised by AV, 9-Jun-2019.) $)
   zring1 $p |- 1 = ( 1r ` ZZring ) $=
     ( cz ccnfld csubrg cfv wcel c1 czring cur wceq zsubrg df-zring cnfld1 ax-mp
     subrg1 ) ABCDEFGHDIJABGFKLNM $.
@@ -267117,9 +267117,8 @@ According to Wikipedia ("Integer", 25-May-2019,
     zrhpsgnevpm.y $e |- Y = ( ZRHom ` R ) $.
     zrhpsgnevpm.s $e |- S = ( pmSgn ` N ) $.
     zrhpsgnevpm.o $e |- .1. = ( 1r ` R ) $.
-    $( The sign of an even permutation embedded into a ring is the
-       multiplicative neutral element of the ring.  (Contributed by SO,
-       9-Jul-2018.) $)
+    $( The sign of an even permutation embedded into a ring is the unity
+       element of the ring.  (Contributed by SO, 9-Jul-2018.) $)
     zrhpsgnevpm $p |- ( ( R e. Ring /\ N e. Fin /\ F e. ( pmEven ` N ) ) ->
         ( ( Y o. S ) ` F ) = .1. ) $=
       ( crg wcel cfn cevpm cfv w3a c1 cbs co wceq eqid ccom csymg cmgp cneg cpr
@@ -267132,8 +267131,8 @@ According to Wikipedia ("Integer", 25-May-2019,
     zrhpsgnodpm.p $e |- P = ( Base ` ( SymGrp ` N ) ) $.
     zrhpsgnodpm.i $e |- I = ( invg ` R ) $.
     $( The sign of an odd permutation embedded into a ring is the additive
-       inverse of the multiplicative neutral element of the ring.  (Contributed
-       by SO, 9-Jul-2018.) $)
+       inverse of the unity element of the ring.  (Contributed by SO,
+       9-Jul-2018.) $)
     zrhpsgnodpm $p |- ( ( R e. Ring /\ N e. Fin /\ F e. ( P \
         ( pmEven ` N ) ) ) -> ( ( Y o. S ) ` F ) = ( I ` .1. ) ) $=
       ( wcel cfv c1 co wceq eqid czring crg cfn cevpm cdif w3a ccom cneg ccnfld
@@ -267451,15 +267450,15 @@ According to Wikipedia ("Integer", 25-May-2019,
     ( cr cvv wcel cmul crefld cmulr wceq reex ccnfld df-refld cnfldmul ressmulr
     cfv ax-mp ) ABCDEFMGHAIEDBJKLN $.
 
-  $( The neutral element of the field of reals.  (Contributed by Thierry
-     Arnoux, 1-Nov-2017.) $)
+  $( The zero element of the field of reals.  (Contributed by Thierry Arnoux,
+     1-Nov-2017.) $)
   re0g $p |- 0 = ( 0g ` RRfld ) $=
     ( ccnfld cmnd wcel cc0 cr wss crefld c0g cfv wceq ccrg crg crngring ringmnd
     cc cncrng mp2b 0re ax-resscn df-refld cnfldbas cnfld0 ress0g mp3an ) ABCZDE
     CEOFDGHIJAKCALCUEPAMANQRSEOAGDTUAUBUCUD $.
 
-  $( The multiplicative neutral element of the field of reals.  (Contributed by
-     Thierry Arnoux, 1-Nov-2017.) $)
+  $( The unity element of the field of reals.  (Contributed by Thierry Arnoux,
+     1-Nov-2017.) $)
   re1r $p |- 1 = ( 1r ` RRfld ) $=
     ( cr ccnfld csubrg cfv wcel c1 crefld cur wceq cdr resubdrg simpli df-refld
     cnfld1 subrg1 ax-mp ) ABCDEZFGHDIQGJEKLABGFMNOP $.
@@ -269195,8 +269194,8 @@ with modules (over rings) instead of vector spaces (over fields) allows for a
   are usually regarded as "over a ring" in this part.
 
   Unless otherwise stated, the rings of scalars need not be commutative
-  (see ~ df-cring ), but the existence of a multiplicative neutral element is
-  always assumed (our rings are unital, see ~ df-ring ).
+  (see ~ df-cring ), but the existence of a unity element is always assumed
+  (our rings are unital, see ~ df-ring ).
 
   For readers knowing vector spaces but unfamiliar with modules: the elements
   of a module are still called "vectors" and they still form a group under
@@ -492583,8 +492582,8 @@ such that every prime ideal contains a prime element (this is a
     sral1r.a $e |- ( ph -> A = ( ( subringAlg ` W ) ` S ) ) $.
     sral1r.1 $e |- ( ph -> .1. = ( 1r ` W ) ) $.
     sral1r.s $e |- ( ph -> S C_ ( Base ` W ) ) $.
-    $( The multiplicative neutral element of a subring algebra.  (Contributed
-       by Thierry Arnoux, 24-Jul-2023.) $)
+    $( The unity element of a subring algebra.  (Contributed by Thierry Arnoux,
+       24-Jul-2023.) $)
     sra1r $p |- ( ph -> .1. = ( 1r ` A ) ) $=
       ( vx vy cur cfv cbs eqidd srabase cv wcel wa cmulr sramulr oveqdr eqtrd
       rngidpropd ) ADEKLBKLGAIJEMLZEBAUDNABCEFHOAIPUDQJPUDQRIJESLBSLABCEFHTUAUC
@@ -674969,7 +674968,7 @@ is in the span of P(i)(X), so there is an R-linear combination of
 
   ${
     $d A x y $.
-    $( A limit ordinal is either the proper class of ordinals or some non-zero
+    $( A limit ordinal is either the proper class of ordinals or some nonzero
        product with omega.  (Contributed by RP, 8-Jan-2025.) $)
     dflim5 $p |- ( Lim A <-> ( A = On \/
                                E. x e. ( On \ 1o ) A = ( _om .o x ) ) ) $=