From 7eb414de9a1270026d40d883aeefa2d60fcb75bd Mon Sep 17 00:00:00 2001
From: Thierry Arnoux <5831830+tirix@users.noreply.github.com>
Date: Tue, 9 Apr 2024 14:21:00 +0200
Subject: [PATCH] Comments wording as per remarks from @savask

---
 set.mm | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/set.mm b/set.mm
index 5ea9b475f7..37539cdac6 100644
--- a/set.mm
+++ b/set.mm
@@ -472220,7 +472220,7 @@ The sumset operation can be used for both group (additive) operations and
     elgrplsmsn.4 $e |- ( ph -> G e. V ) $.
     elgrplsmsn.5 $e |- ( ph -> A C_ B ) $.
     elgrplsmsn.6 $e |- ( ph -> X e. B ) $.
-    $( Membership to a sumset with a singleton for a group operation.
+    $( Membership in a sumset with a singleton for a group operation.
        (Contributed by Thierry Arnoux, 21-Jan-2024.) $)
     elgrplsmsn $p |- ( ph -> ( Z e. ( A .(+) { X } )
                        <-> E. x e. A Z = ( x .+ X ) ) ) $=
@@ -472269,8 +472269,8 @@ The sumset operation can be used for both group (additive) operations and
     elringlsm.5 $e |- ( ph -> G e. V ) $.
     elringlsm.6 $e |- ( ph -> E C_ B ) $.
     elringlsm.7 $e |- ( ph -> F C_ B ) $.
-    $( Membership to a sumset for a ring operation.  (Contributed by Thierry
-       Arnoux, 20-Jan-2024.) $)
+    $( Membership in a product of two subsets of a ring.  (Contributed by
+       Thierry Arnoux, 20-Jan-2024.) $)
     elringlsm $p |- ( ph -> ( Z e. ( E .X. F )
                             <-> E. x e. E E. y e. F Z = ( x .x. y ) ) ) $=
       ( wcel wss co cv wceq wrex wb mgpbas mgpplusg lsmelvalx syl3anc ) AJKTHDU
@@ -472284,8 +472284,8 @@ The sumset operation can be used for both group (additive) operations and
     ringlsmss.4 $e |- ( ph -> R e. Ring ) $.
     ringlsmss.5 $e |- ( ph -> E C_ B ) $.
     ringlsmss.6 $e |- ( ph -> F C_ B ) $.
-    $( Closure for the sumset multiplicative operation in a ring.  (Contributed
-       by Thierry Arnoux, 20-Jan-2024.) $)
+    $( Closure of the product of two subsets of a ring.  (Contributed by
+       Thierry Arnoux, 20-Jan-2024.) $)
     ringlsmss $p |- ( ph -> ( E .X. F ) C_ B ) $=
       ( cmnd wcel wss co crg ringmgp syl mgpbas lsmssv syl3anc ) AGNOZEBPFBPEFD
       QBPACROUDKCGISTLMBDEFGBCGIHUAJUBUC $.
@@ -472300,15 +472300,16 @@ The sumset operation can be used for both group (additive) operations and
     lsmsnpridl.4 $e |- K = ( RSpan ` R ) $.
     lsmsnpridl.5 $e |- ( ph -> R e. Ring ) $.
     lsmsnpridl.6 $e |- ( ph -> X e. B ) $.
-    $( The sumset of a ring with a single element is the element's principal
-       ideal.  (Contributed by Thierry Arnoux, 21-Jan-2024.) $)
+    $( The product of the ring with a single element is equal to the principal
+       ideal generated by that element.  (Contributed by Thierry Arnoux,
+       21-Jan-2024.) $)
     lsmsnpridl $p |- ( ph -> ( B .X. { X } ) = ( K ` { X } ) ) $=
       ( vx vy co cfv cv wcel cvv csn cmulr wceq wrex mgpbas eqid mgpplusg fvexi
       cmgp a1i ssidd elgrplsmsn crg wb rspsnel syl2anc bitr4d eqrdv ) ANBGUAZDP
       ZUSFQZANRZUTSVBORGCUBQZPUCOBUDZVBVASZAOBBVCDETGVBBCEIHUECVCEIVCUFZUGJETSA
       ECUIIUHUJABUKMULACUMSGBSVEVDUNLMOBCVCVBFGHVFKUOUPUQUR $.
 
-    $( The sumset of a ring with a single element is a principal ideal.
+    $( The product of the ring with a single element is a principal ideal.
        (Contributed by Thierry Arnoux, 21-Jan-2024.) $)
     lsmsnidl $p |- ( ph -> ( B .X. { X } ) e. ( LPIdeal ` R ) ) $=
       ( vy csn co cfv wcel wceq wb clpidl cv wrex sneq fveq2d eqeq2d lsmsnpridl
@@ -472324,7 +472325,7 @@ The sumset operation can be used for both group (additive) operations and
     lsmidl.5 $e |- ( ph -> R e. Ring ) $.
     lsmidl.6 $e |- ( ph -> I e. ( LIdeal ` R ) ) $.
     lsmidl.7 $e |- ( ph -> J e. ( LIdeal ` R ) ) $.
-    $( The sumset sum of two ideals is the ideal generated by their union.
+    $( The sum of two ideals is the ideal generated by their union.
        (Contributed by Thierry Arnoux, 21-Jan-2024.) $)
     lsmidllsp $p |- ( ph -> ( I .(+) J ) = ( K ` ( I u. J ) ) ) $=
       ( co cfv clsm crg wcel wceq syl crglmod rlmlsm syl5eq oveqd clmod rlmlmod
@@ -472332,8 +472333,8 @@ The sumset operation can be used for both group (additive) operations and
       NEFDUAOZPOZNZEFUGGOZACUSEFACDPOZUSIADQRZVBUSSKDQUBTUCUDAURUERZEDUHOZRFVER
       UTVASAVCVDKDUFTLMUSVEEFGURDUIGDUJOURUKOJDULUMUSUNUOUPUQ $.
 
-    $( The sumset sum of two ideals is an ideal.  (Contributed by Thierry
-       Arnoux, 21-Jan-2024.) $)
+    $( The sum of two ideals is an ideal.  (Contributed by Thierry Arnoux,
+       21-Jan-2024.) $)
     lsmidl $p |- ( ph -> ( I .(+) J ) e. ( LIdeal ` R ) ) $=
       ( cfv wcel wss syl lidlss cbs eqtri cun clidl lsmidllsp crglmod clmod crg
       rlmlmod eqid unssd rlmbas lidlval crsp clspn rspval lspcl syl2anc eqeltrd