nonunital -> non-unital

set.mm

@@ -775117,7 +775117,7 @@ Nonzero rings (extension)
     rngdi.b $e |- B = ( Base ` R ) $.
     rngdi.p $e |- .+ = ( +g ` R ) $.
     rngdi.t $e |- .x. = ( .r ` R ) $.
-    $( Distributive law for the multiplication operation of a nonunital ring
+    $( Distributive law for the multiplication operation of a non-unital ring
        (right-distributivity).  (Contributed by AV, 17-Apr-2020.) $)
     rngdir $p |- ( ( R e. Rng /\ ( X e. B /\ Y e. B /\ Z e. B ) ) ->
                      ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) $=
@@ -775137,15 +775137,15 @@ Nonzero rings (extension)
   ${
     rngcl.b $e |- B = ( Base ` R ) $.
     rngcl.t $e |- .x. = ( .r ` R ) $.
-    $( Closure of the multiplication operation of a nonunital ring.
+    $( Closure of the multiplication operation of a non-unital ring.
        (Contributed by AV, 17-Apr-2020.) $)
     rngcl $p |- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B ) $=
       ( crng wcel cmgp cfv cmgm csgrp eqid rngmgp sgrpmgm syl mgpbas mgpplusg
       co mgmcl syl3an1 ) BHIZBJKZLIZDAIEAIDECTAIUCUDMIUEBUDUDNZOUDPQAUDDECABUDU
       FFRBCUDUFGSUAUB $.
 
     rnglz.z $e |- .0. = ( 0g ` R ) $.
-    $( The zero of a nonunital ring is a left-absorbing element.  (Contributed
+    $( The zero of a non-unital ring is a left-absorbing element.  (Contributed
        by AV, 17-Apr-2020.) $)
     rnglz $p |- ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .0. ) $=
       ( crng wcel wa co cplusg cfv wceq cgrp cabl syl adantr syl2anc rngabl w3a
@@ -775504,8 +775504,8 @@ Nonzero rings (extension)
       GVHABFVRVHVRFDULPZDVRFWATHVRTZUMUNUQUOUPVGVLURKVMURKZVSVNKVHCVLVLTZUSVHVJ
       WCVPDVMVMTZUSSABVLVMVSVRBCVLWDGUTDVRVMWEWBVAVSTVBUHVCVDCDEVLVMWDWEVEVF $.
 
-    $( The constant mapping to zero is a nonunital ring homomorphism from any
-       nonunital ring to the zero ring.  (Contributed by AV, 17-Apr-2020.) $)
+    $( The constant mapping to zero is a non-unital ring homomorphism from any
+       non-unital ring to the zero ring.  (Contributed by AV, 17-Apr-2020.) $)
     c0rnghm $p |- ( ( S e. Rng /\ T e. ( Ring \ NzRing ) )
                     -> H e. ( S RngHomo T ) ) $=
       ( crng wcel crg cnzr wa co cmgp cfv cgrp syl eqid cdif cghm wss ringssrng
@@ -775578,8 +775578,8 @@ Nonzero rings (extension)
         CUEUHUIUJUK $.
     $}
 
-    $( The constant mapping to zero is a nonunital ring homomorphism from the
-       zero ring to any nonunital ring.  (Contributed by AV, 17-Apr-2020.) $)
+    $( The constant mapping to zero is a non-unital ring homomorphism from the
+       zero ring to any non-unital ring.  (Contributed by AV, 17-Apr-2020.) $)
     zrrnghm $p |- ( ( S e. Rng /\ T e. ( Ring \ NzRing ) )
                     -> H e. ( T RngHomo S ) ) $=
       ( va vc wcel wa co cfv wceq wral syl adantr eqid crng crg cnzr cdif cmulr
@@ -776993,7 +776993,7 @@ underlying set (base set) and the morphisms (non-unital ring
     zrinitorngc.c $e |- C = ( RngCat ` U ) $.
     zrinitorngc.z $e |- ( ph -> Z e. ( Ring \ NzRing ) ) $.
     zrinitorngc.e $e |- ( ph -> Z e. U ) $.
-    $( The zero ring is an initial object in the category of nonunital rings.
+    $( The zero ring is an initial object in the category of non-unital rings.
        (Contributed by AV, 18-Apr-2020.) $)
     zrinitorngc $p |- ( ph -> Z e. ( InitO ` C ) ) $=
       ( vh vr vx cfv wcel wa wceq crng eqid eleq2d adantr va cinito cv chom weu
@@ -777016,7 +777016,7 @@ underlying set (base set) and the morphisms (non-unital ring
       UUKWQXTWLNUUKUUIWBWOVSWPWRWSWTTXAXBWSXNYDJYAYBXJYAXMXCXDWIXEAXPBJXLEKYMYT
       AYSBXFNFBCDGXGWIUUAXIXH $.
 
-    $( The zero ring is a terminal object in the category of nonunital rings.
+    $( The zero ring is a terminal object in the category of non-unital rings.
        (Contributed by AV, 17-Apr-2020.) $)
     zrtermorngc $p |- ( ph -> Z e. ( TermO ` C ) ) $=
       ( vh vr vx cfv wcel cv wa wceq crng eqid adantr va ctermo chom co weu cbs