diff --git a/set.mm b/set.mm
index 4cfaefb59..37539cdac 100644
--- a/set.mm
+++ b/set.mm
@@ -250882,6 +250882,17 @@ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) $=
     csca id eqid islvec sylanbrc ) ABCZADEZFCZTNEZBCTGCSAHCUAAIAJKSAUBBABLSOMUB
     TUBPQR $.
 
+  ${
+    $d R t u x y $.
+    $( Subgroup sum of the ring module.  (Contributed by Thierry Arnoux,
+       9-Apr-2024.) $)
+    rlmlsm $p |- ( R e. V -> ( LSSum ` R ) = ( LSSum ` ( ringLMod ` R ) ) ) $=
+      ( vt vu vx vy wcel clsm cfv cbs cpw cv cplusg co cmpo crn crglmod lsmfval
+      eqid cvv wceq fvex rlmbas rlmplusg mp1i eqtr4d ) ABGZAHIZCDAJIZKZUJEFCLDL
+      ELFLAMIZNOPOZAQIZHIZEFDCUIUKUHABUISUKSUHSRUMTGUNULUAUGAQUBEFDCUIUKUNUMTAU
+      CAUDUNSRUEUF $.
+  $}
+
   ${
     $d x y R $.
     $( Vector negation in the ring module.  (Contributed by Stefan O'Rear,
@@ -436874,6 +436885,15 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
 htmldef "PrmIdeal" as "PrmIdeal";
   althtmldef "PrmIdeal" as "PrmIdeal";
   latexdef "PrmIdeal" as "\mathrm{PrmIdeal}";
+htmldef "MaxIdeal" as "MaxIdeal";
+  althtmldef "MaxIdeal" as "MaxIdeal";
+  latexdef "MaxIdeal" as "\mathrm{MaxIdeal}";
+htmldef "IDLsrg" as "IDLsrg";
+  althtmldef "IDLsrg" as "IDLsrg";
+  latexdef "IDLsrg" as "\mathrm{IDLsrg}";
+htmldef "Spec" as "Spec";
+  althtmldef "Spec" as "Spec";
+  latexdef "Spec" as "\mathrm{Spec}";
 htmldef "subMat1" as "subMat1";
   althtmldef "subMat1" as "subMat1";
   latexdef "subMat1" as "\mathrm{subMat1}";
@@ -461638,6 +461658,32 @@ its graph has a given second element (that is, function value).
       JUUOYMUMYKYN $.
   $}
 
+  ${
+    fvdifsupp.1 $e |- ( ph -> F Fn A ) $.
+    fvdifsupp.2 $e |- ( ph -> A e. V ) $.
+    fvdifsupp.3 $e |- ( ph -> Z e. W ) $.
+    fvdifsupp.4 $e |- ( ph -> X e. ( A \ ( F supp Z ) ) ) $.
+    $( Function value is zero outside of its support.  (Contributed by Thierry
+       Arnoux, 21-Jan-2024.) $)
+    fvdifsupp $p |- ( ph -> ( F ` X ) = Z ) $=
+      ( cfv wceq csupp co wcel wn eldifbd wne eldifad elsuppfn syl3anc mpbirand
+      wfn wa wb necon2bbid mpbird ) AFCLZGMFCGNOZPZQAFBUJKRAUKUIGAUKFBPZUIGSZAF
+      BUJKTACBUDBDPGEPUKULUMUEUFHIJFCDEBGUAUBUCUGUH $.
+  $}
+
+  ${
+    $d A x $.  $d C x $.
+    fmptssfisupp.1 $e |- ( ph -> ( x e. A |-> B ) finSupp Z ) $.
+    fmptssfisupp.2 $e |- ( ph -> C C_ A ) $.
+    fmptssfisupp.3 $e |- ( ph -> Z e. V ) $.
+    $( The restriction of a mapping function has finite support if that
+       function has finite support.  (Contributed by Thierry Arnoux,
+       21-Jan-2024.) $)
+    fmptssfisupp $p |- ( ph -> ( x e. C |-> B ) finSupp Z ) $=
+      ( cmpt cres cfsupp resmptd fsuppres eqbrtrrd ) ABCDKZELBEDKGMABCEDINAQFEG
+      HJOP $.
+  $}
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -472151,6 +472197,153 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
   $}
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Subgroup sum / Sumset / Minkowski sum
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+
+  The sumset (also called the Minkowski sum) of two subsets ` A ` and ` B ` ,
+  is defined to be the set of all sums of an element from ` A ` with an element
+  from ` B ` .
+
+  The sumset operation can be used for both group (additive) operations and
+  ring (multiplicative) operations.
+
+$)
+
+  ${
+    $d .+ x y $.  $d A x y $.  $d B x y $.  $d G x y $.  $d X x y $.
+    $d Z x y $.  $d ph x $.
+    elgrplsmsn.1 $e |- B = ( Base ` G ) $.
+    elgrplsmsn.2 $e |- .+ = ( +g ` G ) $.
+    elgrplsmsn.3 $e |- .(+) = ( LSSum ` G ) $.
+    elgrplsmsn.4 $e |- ( ph -> G e. V ) $.
+    elgrplsmsn.5 $e |- ( ph -> A C_ B ) $.
+    elgrplsmsn.6 $e |- ( ph -> X e. B ) $.
+    $( 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 ) ) ) $=
+      ( vy co wcel wceq csn cv wrex wss wb snssd lsmelvalx syl3anc oveq2 eqeq2d
+      rexsng syl rexbidv bitrd ) AJCIUAZFRSZJBUBZQUBZERZTZQUOUCZBCUCZJUQIERZTZB
+      CUCAGHSCDUDUODUDUPVBUENOAIDPUFBQDEFCUOGHJKLMUGUHAVAVDBCAIDSVAVDUEPUTVDQID
+      URITUSVCJURIUQEUIUJUKULUMUN $.
+  $}
+
+  ${
+    $d .(+) k $.  $d .+ g $.  $d .+ h x y $.  $d .~ h k $.  $d A g h k x y $.
+    $d B h x y $.  $d G h $.  $d X g h k $.  $d X g h x y $.  $d h k ph $.
+    lsmsnorb.1 $e |- B = ( Base ` G ) $.
+    lsmsnorb.2 $e |- .+ = ( +g ` G ) $.
+    lsmsnorb.3 $e |- .(+) = ( LSSum ` G ) $.
+    lsmsnorb.4 $e |- .~ = { <. x , y >. | ( { x , y } C_ B
+                                             /\ E. g e. A ( g .+ x ) = y ) } $.
+    lsmsnorb.5 $e |- ( ph -> G e. Mnd ) $.
+    lsmsnorb.6 $e |- ( ph -> A C_ B ) $.
+    lsmsnorb.7 $e |- ( ph -> X e. B ) $.
+    $( The sumset of a group with a single element is the element's orbit by
+       the group action.  See ~ gaorb .  (Contributed by Thierry Arnoux,
+       21-Jan-2024.) $)
+    lsmsnorb $p |- ( ph -> ( A .(+) { X } ) = [ X ] .~ ) $=
+      ( vh wcel vk csn co cec cv cmnd wss snssd lsmssv syl3anc sselda df-ec crn
+      cima imassrn cpr wceq wrex wa copab rneqi wex cab rnopab vex prss biimpri
+      simprd adantr exlimiv abssi eqsstri a1i eqsstrid wbr w3a anim1i biantrurd
+      sstri df-3an syl6bbr gaorb syl6rbbr cvv wb elecg sylancr elgrplsmsn eqcom
+      rexbii syl6bb 3bitr4rd eqrdav ) AUADKUBZGUCZKHUDZEAWOEUAUEZAJUFTZDEUGZWNE
+      UGWOEUGPQAKERUHEGDWNJLNUIUJUKAWPEWQAWPHWNUNZEKHULWTEUGAWTHUMZEHWNUOXABUEZ
+      CUEZUPEUGZIUEXBFUCXCUQIDURZUSZBCUTZUMZEHXGOVAXHXFBVBZCVCEXFBCVDXICEXFXCET
+      ZBXDXJXEXDXBETZXJXKXJUSXDXBXCEBVECVEVFVGVHVIVJVKVLVLVSVMVNUKAWQETZUSZKWQH
+      VOZSUEKFUCZWQUQZSDURZWQWPTZWQWOTZXMXQKETZXLXQVPZXNXMXQXTXLUSZXQUSYAXMYBXQ
+      AXTXLRVQVRXTXLXQVTWABCKWQFHISDEOWBWCXMWQWDTXTXRXNWEUAVEAXTXLRVIZWQKHWDEWF
+      WGXMXSWQXOUQZSDURXQXMSDEFGJUFKWQLMNAWRXLPVIAWSXLQVIYCWHYDXPSDWQXOWIWJWKWL
+      WM $.
+  $}
+
+  ${
+    $d .x. x y $.  $d B x y $.  $d E x y $.  $d F x y $.  $d G x y $.
+    $d Z x y $.
+    elringlsm.1 $e |- B = ( Base ` R ) $.
+    elringlsm.2 $e |- .x. = ( .r ` R ) $.
+    elringlsm.3 $e |- G = ( mulGrp ` R ) $.
+    elringlsm.4 $e |- .X. = ( LSSum ` G ) $.
+    elringlsm.5 $e |- ( ph -> G e. V ) $.
+    elringlsm.6 $e |- ( ph -> E C_ B ) $.
+    elringlsm.7 $e |- ( ph -> F C_ B ) $.
+    $( 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
+      AIDUALHIGUBTLBUCCUCFUBUDCIUEBHUEUFQRSBCDFGHIJKLDEJOMUGEFJONUHPUIUJ $.
+  $}
+
+  ${
+    ringlsmss.1 $e |- B = ( Base ` R ) $.
+    ringlsmss.2 $e |- G = ( mulGrp ` R ) $.
+    ringlsmss.3 $e |- .X. = ( LSSum ` G ) $.
+    ringlsmss.4 $e |- ( ph -> R e. Ring ) $.
+    ringlsmss.5 $e |- ( ph -> E C_ B ) $.
+    ringlsmss.6 $e |- ( ph -> F C_ B ) $.
+    $( 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 $.
+  $}
+
+  ${
+    $d .X. x y $.  $d B x y $.  $d G y $.  $d K x y $.  $d R y $.  $d X x y $.
+    $d ph x $.  $d ph y $.
+    lsmsnpridl.1 $e |- B = ( Base ` R ) $.
+    lsmsnpridl.2 $e |- G = ( mulGrp ` R ) $.
+    lsmsnpridl.3 $e |- .X. = ( LSSum ` G ) $.
+    lsmsnpridl.4 $e |- K = ( RSpan ` R ) $.
+    lsmsnpridl.5 $e |- ( ph -> R e. Ring ) $.
+    lsmsnpridl.6 $e |- ( ph -> X e. B ) $.
+    $( 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 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
+      adantl rspcedvd crg eqid islpidl syl mpbird ) ABGOZDPZCUAQZRZUPNUBZOZFQZS
+      ZNBUCZAVBUPUOFQZSZNGBMUSGSZVBVETAVFVAVDUPVFUTUOFUSGUDUEUFUHABCDEFGHIJKLMU
+      GUIACUJRURVCTLBUQCNUPFUQUKKHULUMUN $.
+  $}
+
+  ${
+    lsmidl.1 $e |- B = ( Base ` R ) $.
+    lsmidl.3 $e |- .(+) = ( LSSum ` R ) $.
+    lsmidl.4 $e |- K = ( RSpan ` R ) $.
+    lsmidl.5 $e |- ( ph -> R e. Ring ) $.
+    lsmidl.6 $e |- ( ph -> I e. ( LIdeal ` R ) ) $.
+    lsmidl.7 $e |- ( ph -> J e. ( LIdeal ` R ) ) $.
+    $( 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
+      cun clidl lidlval crsp clspn rspval eqtri eqid lsmsp syl3anc eqtrd ) AEFC
+      NEFDUAOZPOZNZEFUGGOZACUSEFACDPOZUSIADQRZVBUSSKDQUBTUCUDAURUERZEDUHOZRFVER
+      UTVASAVCVDKDUFTLMUSVEEFGURDUIGDUJOURUKOJDULUMUSUNUOUPUQ $.
+
+    $( 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
+      co ) AEFCUREFUAZGNZDUBNZABCDEFGHIJKLMUCADUDNZUEOZUSBPUTVAOADUFOVCKDUGQAEF
+      BAEVAOEBPLBEVADHVAUHZRQAFVAOFBPMBFVADHVDRQUIVAUSGBVBBDSNVBSNHDUJTDUKGDULN
+      VBUMNJDUNTUOUPUQ $.
+  $}
+
+
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
   Prime Ideals
@@ -472322,6 +472515,20 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
       XBXAXTRZYARZYHXJYKXKUVOXFYGMZYHXJUVNUVPYAXAXQXTUVPXRCEXFYFGUUAWFSWHYGDXFW
       IWJUVOXGYJMZYKXKXAYAUVQXTXAXQYAUVQXRCEXGYFGUUAWFSWKYJDXGWIWJWLWMWHWNWOWCW
       DWRXAXQXOXBXRXOXQXDXEXNRZRXBXDXEXNWPXQXDUVRXBABCDEFGHWQWCWSSWT $.
+
+    $d .x. a b $.  $d B a b $.  $d I a b $.  $d J a b $.  $d P a b $.
+    $d R a b $.
+    $( Property of a prime ideal in a commutative ring.  (Contributed by Jeff
+       Madsen, 17-Jun-2011.)  (Revised by Thierry Arnoux, 12-Jan-2024.) $)
+    prmidlc $p |- ( ( ( R e. CRing /\ P e. ( PrmIdeal ` R ) ) /\ ( I e. B /\ J
+       e. B /\ ( I .x. J ) e. P ) ) -> ( I e. P \/ J e. P ) ) $=
+      ( va vb wcel cfv wa co w3a cv wo wi wral eleq1d ccrg cprmidl simpr1 clidl
+      simpr2 wne isprmidlc biimpa simp3d adantr simpr3 wceq simpl simpr orbi12d
+      oveq12 imbi12d rspc2gv imp31 syl1111anc ) CUAKZBCUBLKZMZEAKZFAKZEFDNZBKZO
+      ZMVDVEIPZJPZDNZBKZVIBKZVJBKZQZRZJASIASZVGEBKZFBKZQZVCVDVEVGUCVCVDVEVGUEVC
+      VQVHVCBCUDLKZBAUFZVQVAVBWAWBVQOIJABCDGHUGUHUIUJVCVDVEVGUKVDVEMVQVGVTVPVGV
+      TRIJEFAAVIEULZVJFULZMZVLVGVOVTWEVKVFBVIEVJFDUPTWEVMVRVNVSWEVIEBWCWDUMTWEV
+      JFBWCWDUNTUOUQURUSUT $.
   $}
 
   ${
@@ -472429,6 +472636,199 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a
   $}
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Maximal Ideals
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  $c MaxIdeal $.
+
+  $( Extend class notation with the class of maximal ideals. $)
+  cmxidl $a class MaxIdeal $.
+
+  ${
+    $d r i j $.
+    $( Define the class of maximal ideals of a ring ` R ` .  A proper ideal is
+       called maximal if it is maximal with respect to inclusion among proper
+       ideals.  (Contributed by Jeff Madsen, 5-Jan-2011.)  (Revised by Thierry
+       Arnoux, 19-Jan-2024.) $)
+    df-mxidl $a |- MaxIdeal = ( r e. Ring |->
+            { i e. ( LIdeal ` r ) | ( i =/= ( Base ` r ) /\ A. j e. ( LIdeal `
+              r ) ( i C_ j -> ( j = i \/ j = ( Base ` r ) ) ) ) } ) $.
+  $}
+
+  ${
+    $d B r $.  $d R i j r $.
+    mxidlval.1 $e |- B = ( Base ` R ) $.
+    $( The set of maximal ideals of a ring.  (Contributed by Jeff Madsen,
+       5-Jan-2011.)  (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    mxidlval $p |- ( R e. Ring -> ( MaxIdeal ` R ) = { i e. ( LIdeal ` R ) | (
+       i =/= B /\ A. j e. ( LIdeal ` R ) ( i C_ j -> ( j = i \/ j = B ) ) ) } )
+       $=
+      ( vr cv cbs cfv wne wss wceq wo wi clidl wral wa crab crg fveq2 raleqbidv
+      cmxidl syl6eqr neeq2d eqeq2d orbi2d anbi12d rabeqbidv df-mxidl fvex rabex
+      imbi2d fvmpt ) FBCGZFGZHIZJZUNDGZKZURUNLZURUPLZMZNZDUOOIZPZQZCVDRUNAJZUSU
+      TURALZMZNZDBOIZPZQZCVKRSUBUOBLZVFVMCVDVKUOBOTZVNUQVGVEVLVNUPAUNVNUPBHIAUO
+      BHTEUCZUDVNVCVJDVDVKVOVNVBVIUSVNVAVHUTVNUPAURVPUEUFULUAUGUHCDFUIVMCVKBOUJ
+      UKUM $.
+
+    $d B i $.  $d M i j $.  $d R i j $.
+    $( The predicate "is a maximal ideal".  (Contributed by Jeff Madsen,
+       5-Jan-2011.)  (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    ismxidl $p |- ( R e. Ring -> ( M e. ( MaxIdeal ` R ) <-> ( M e. ( LIdeal `
+       R ) /\ M =/= B /\ A. j e. ( LIdeal ` R ) ( M C_ j -> ( j = M \/ j = B )
+       ) ) ) ) $=
+      ( vi crg wcel cmxidl cfv cv wne wss wceq wo wi clidl wral wa crab imbi12d
+      w3a mxidlval eleq2d neeq1 sseq1 eqeq2 orbi1d ralbidv anbi12d elrab 3anass
+      bitr4i syl6bb ) BGHZDBIJZHDFKZALZUQCKZMZUSUQNZUSANZOZPZCBQJZRZSZFVETZHZDV
+      EHZDALZDUSMZUSDNZVBOZPZCVERZUBZUOUPVHDABFCEUCUDVIVJVKVPSZSVQVGVRFDVEUQDNZ
+      URVKVFVPUQDAUEVSVDVOCVEVSUTVLVCVNUQDUSUFVSVAVMVBUQDUSUGUHUAUIUJUKVJVKVPUL
+      UMUN $.
+
+    $( A maximal ideal is an ideal.  (Contributed by Jeff Madsen, 5-Jan-2011.)
+       (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    mxidlidl $p |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M e. ( LIdeal `
+       R ) ) $=
+      ( vj crg wcel cmxidl cfv wa clidl wne cv wss wceq wo wi wral w3a ismxidl
+      biimpa simp1d ) BFGZCBHIGZJCBKIZGZCALZCEMZNUHCOUHAOPQEUERZUCUDUFUGUISABEC
+      DTUAUB $.
+
+    $( A maximal ideal is proper.  (Contributed by Jeff Madsen, 16-Jun-2011.)
+       (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    mxidlnr $p |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> M =/= B ) $=
+      ( vj crg wcel cmxidl cfv wa clidl wne cv wss wceq wo wi wral w3a ismxidl
+      biimpa simp2d ) BFGZCBHIGZJCBKIZGZCALZCEMZNUHCOUHAOPQEUERZUCUDUFUGUISABEC
+      DTUAUB $.
+
+    $d B j $.  $d I j $.
+    $( A maximal ideal is a maximal proper ideal.  (Contributed by Jeff Madsen,
+       16-Jun-2011.)  (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    mxidlmax $p |- ( ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) )
+         /\ ( I e. ( LIdeal ` R ) /\ M C_ I ) ) -> ( I = M \/ I = B ) ) $=
+      ( vj crg wcel cmxidl cfv wa clidl wss wceq wo cv wi sseq2 eqeq1 orbi12d
+      imbi12d wral wne w3a ismxidl biimpa simp3d adantr simpr rspcdva impr ) BG
+      HZDBIJHZKZCBLJZHZDCMZCDNZCANZOZUNUPKDFPZMZVADNZVAANZOZQZUQUTQFUOCVACNZVBU
+      QVEUTVACDRVGVCURVDUSVACDSVACASTUAUNVFFUOUBZUPUNDUOHZDAUCZVHULUMVIVJVHUDAB
+      FDEUEUFUGUHUNUPUIUJUK $.
+
+    ${
+      mxidln1.1 $e |- .1. = ( 1r ` R ) $.
+      $( One is not contained in any maximal ideal.  (Contributed by Jeff
+         Madsen, 17-Jun-2011.)  (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+      mxidln1 $p |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> -. .1. e. M )
+      $=
+        ( crg wcel cmxidl cfv wa wn mxidlnr clidl wceq wb mxidlidl eqid lidl1el
+        wne syldan necon3bbid mpbird ) BGHZDBIJHZKZCDHZLDATABDEMUFUGDAUDUEDBNJZ
+        HUGDAOPABDEQABUHCDUHREFSUAUBUC $.
+    $}
+
+    $( A ring with a maximal ideal is a nonzero ring.  (Contributed by Jeff
+       Madsen, 17-Jun-2011.)  (Revised by Thierry Arnoux, 19-Jan-2024.) $)
+    mxidlnzr $p |- ( ( R e. Ring /\ M e. ( MaxIdeal ` R ) ) -> R e. NzRing ) $=
+      ( crg wcel cmxidl cfv cur c0g wne cnzr wa wn mxidlidl eqid lidl0cl syldan
+      clidl mxidln1 nelne2 syl2anc necomd isnzr biimpri ) BEFZCBGHFZBIHZBJHZKZB
+      LFZUFUGMZUIUHULUICFZUHCFNUIUHKUFUGCBSHZFUMABCDOBUNCUIUNPUIPZQRABUHCDUHPZT
+      UIUHCUAUBUCUKUFUJMBUHUIUPUOUDUER $.
+  $}
+
+  ${
+    $d .X. a k u $.  $d .X. b $.  $d M a k u x y $.  $d M b $.  $d R a b x y $.
+    $d R a k u x y $.
+    mxidlprm.1 $e |- .X. = ( LSSum ` ( mulGrp ` R ) ) $.
+    $( Every maximal ideal is prime.  Statement in [Lang] p. 92 (Contributed by
+       Thierry Arnoux, 21-Jan-2024.) $)
+    mxidlprm $p |- ( ( R e. CRing /\ M e. ( MaxIdeal ` R ) )
+                  -> M e. ( PrmIdeal ` R ) ) $=
+      ( va vb wcel cfv wa cv co eqid wceq syl2anc wss syl syl3anc syl22anc wrex
+      wb vx vy vu vk ccrg cmxidl crg clidl cbs wne cmulr wo wi cprmidl crngring
+      wral adantr mxidlidl sylan mxidlnr wn cur cplusg csn simpllr simpr oveq2d
+      eqtrd oveq1d ad4antr ad5antr simp-8r lidlss simp-5r sseldd simplr simp-4r
+      ringlidm ringcl ringdir syl13anc 3eqtr3d simp-10l crngcom lidlmcl ringass
+      eqeltrrd simp-7r eqeltrd lidlacl cmgp cvv mgpplusg fvexd ssidd elgrplsmsn
+      mgpbas ad3antrrr mpbid r19.29a clsm ringidcl clpidl lpiss lsmsnidl lsmidl
+      crsp cun crglmod clmod rlmlmod rlmbas lspssid snssd ringlsmss unssd ssun1
+      rspval a1i lspss sstrd lsmidllsp sseqtrrd mxidlmax lidl0cl eqeq2d rexbidv
+      c0g oveq1 adantl eqcomd rspcedvd mpbird oveq2 cgrp ringgrp grplid simp-5l
+      lsmelvalx ex nelne1 neneqd unitresr eleqtrrd r19.29vva ralrimivva prmidl2
+      orrd anasss ) AUEGZCAUFHGZIZAUGGZCAUHHZGZCAUIHZUJZUAJZUBJZAUKHZKZCGZUURCG
+      ZUUSCGZULZUMZUBUUPUPUAUUPUPCAUNHGUUJUUMUUKAUOZUQZUUJUUMUUKUUOUVGUUPACUUPL
+      ZURZUSZUUJUUMUUKUUQUVGUUPACUVIUTUSUULUVFUAUBUUPUUPUULUURUUPGZUUSUUPGZUVFU
+      ULUVLIZUVMIZUVBUVEUVOUVBIZUVCUVDUVPUVCVAZUVDUVPUVQIZAVBHZUCJZUDJZAVCHZKZM
+      ZUVDUCUDCUUPUURVDZBKZUVRUVTCGZIZUWAUWFGZIZUWDIZUWAEJZUURUUTKZMZUVDEUUPUWK
+      UWLUUPGZIZUWNIZUUSUVTUUSUUTKZUWMUUSUUTKZUWBKZCUWQUVSUUSUUTKZUVTUWMUWBKZUU
+      SUUTKZUUSUWTUWQUVSUXBUUSUUTUWQUVSUWCUXBUWJUWDUWOUWNVEUWQUWAUWMUVTUWBUWPUW
+      NVFVGVHVIUWQUUMUVMUXAUUSMUVRUUMUWGUWIUWDUWOUWNUULUUMUVLUVMUVBUVQUVHVJZVKZ
+      UVNUVMUVBUVQUWGUWIUWDUWOUWNVLZUUPAUUTUVSUUSUVIUUTLZUVSLZVRNUWQUUMUVTUUPGZ
+      UWMUUPGZUVMUXCUWTMUXEUWQCUUPUVTUVRCUUPOZUWGUWIUWDUWOUWNUULUXKUVLUVMUVBUVQ
+      UULUUOUXKUVKUUPCUUNAUVIUUNLZVMPVJZVKUVRUWGUWIUWDUWOUWNVNZVOZUWQUUMUWOUVLU
+      XJUXEUWKUWOUWNVPZUVRUVLUWGUWIUWDUWOUWNUULUVLUVMUVBUVQVQZVKZUUPAUUTUWLUURU
+      VIUXGVSQUXFUUPUWBAUUTUVTUWMUUSUVIUWBLZUXGVTWAWBUWQUUMUUOUWRCGUWSCGUWTCGUX
+      EUVRUUOUWGUWIUWDUWOUWNUVRUUMUUKUUOUXDUUJUUKUVLUVMUVBUVQVNZUVJNZVKZUWQUUSU
+      VTUUTKZUWRCUWQUUJUVMUXIUYCUWRMUUJUUKUVLUVMUVBUVQUWGUWIUWDUWOUWNWCUXFUXOUU
+      PAUUTUUSUVTUVIUXGWDQUWQUUMUUOUVMUWGUYCCGUXEUYBUXFUXNUUPAUUTUUNCUUSUVTUXLU
+      VIUXGWERWGUWQUWSUWLUVAUUTKZCUWQUUMUWOUVLUVMUWSUYDMUXEUXPUXRUXFUUPAUUTUWLU
+      URUUSUVIUXGWFWAUWQUUMUUOUWOUVBUYDCGUXEUYBUXPUVOUVBUVQUWGUWIUWDUWOUWNWHUUP
+      AUUTUUNCUWLUVAUXLUVIUXGWERWIUWBAUUNCUWRUWSUXLUXSWJRWIUWKUWIUWNEUUPSZUWHUW
+      IUWDVPUVRUWIUYETUWGUWIUWDUVREUUPUUPUUTBAWKHZWLUURUWAUUPAUYFUYFLZUVIWQZAUU
+      TUYFUYGUXGWMZDUVRAWKWNZUVRUUPWOZUXQWPWRWSWTUVRUVSCUWFAXAHZKZGZUWDUDUWFSUC
+      CSZUVRUVSUUPUYMUVRUUMUVSUUPGUXDUUPAUVSUVIUXHXBPZUVRUYMCMZUYMUUPMZUVRUUMUU
+      KUYMUUNGCUYMOUYQUYRULUXDUXTUVRUUPUYLACUWFAXGHZUVIUYLLZUYSLZUXDUYAUVRAXCHZ
+      UUNUWFUVRUUMVUBUUNOUXDVUBAUUNVUBLUXLXDPUVRUUPABUYFUYSUURUVIUYGDVUAUXDUXQX
+      EVOZXFUVRCCUWFXHZUYSHZUYMUVRCCUYSHZVUEUVRAXIHZXJGZUXKCVUFOUVRUUMVUHUXDAXK
+      PZUXMCUYSUUPVUGAXLZAXRZXMNUVRVUHVUDUUPOCVUDOZVUFVUEOVUIUVRCUWFUUPUXMUVRUU
+      PABUUPUWEUYFUVIUYGDUXDUYKUVRUURUUPUXQXNXOZXPVULUVRCUWFXQXSCVUDUYSUUPVUGVU
+      JVUKXTQYAUVRUUPUYLACUWFUYSUVIUYTVUAUXDUYAVUCYBYCUUPAUYMCUVIYDRUVRUYMCUVRU
+      URUYMGZUVQUYMCUJUVRVUNUURUWLFJZUWBKZMZFUWFSZECSZUVRVURUURAYHHZVUOUWBKZMZF
+      UWFSZEVUTCUVRUUMUUOVUTCGUXDUYAAUUNCVUTUXLVUTLZYENUWLVUTMZVURVVCTUVRVVEVUQ
+      VVBFUWFVVEVUPVVAUURUWLVUTVUOUWBYIYFYGYJUVRVVBUURVUTUURUWBKZMZFUURUWFUVRUU
+      RUWFGUURUWMMZEUUPSUVRVVHUURUVSUURUUTKZMZEUVSUUPUYPUWLUVSMZVVHVVJTUVRVVKUW
+      MVVIUURUWLUVSUURUUTYIYFYJUVRVVIUURUVRUUMUVLVVIUURMUXDUXQUUPAUUTUVSUURUVIU
+      XGUXHVRNYKYLUVREUUPUUPUUTBUYFWLUURUURUYHUYIDUYJUYKUXQWPYMVUOUURMZVVBVVGTU
+      VRVVLVVAVVFUURVUOUURVUTUWBYNYFYJUVRVVFUURUVRAYOGZUVLVVFUURMUVRUUMVVMUXDAY
+      PPUXQUUPUWBAUURVUTUVIUXSVVDYQNYKYLYLUVRUUJUXKUWFUUPOZVUNVUSTUUJUUKUVLUVMU
+      VBUVQYRZUXMVUMEFUUPUWBUYLCUWFAUEUURUVIUXSUYTYSQYMUVPUVQVFUURUYMCUUANUUBUU
+      CUUDUVRUUJUXKVVNUYNUYOTVVOUXMVUMUCUDUUPUWBUYLCUWFAUEUVSUVIUXSUYTYSQWSUUEY
+      TUUHYTUUIUUFUAUBUUPCAUUTUVIUXGUUGR $.
+  $}
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  The semiring of ideals of a ring
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  $c IDLsrg Spec $.
+
+  $( Extend class notation with the semiring of ideals of a ring. $)
+  cidlsrg $a class IDLsrg $.
+
+  ${
+    $d r b i j $.
+    $( Define a structure for the ideals of a ring.  (Contributed by Thierry
+       Arnoux, 21-Jan-2024.) $)
+    df-idlsrg $a |- IDLsrg = ( r e. Ring |-> [_ ( LIdeal ` r ) / b ]_
+        ( { <. ( Base ` ndx ) , b >. ,
+            <. ( +g ` ndx ) ,
+                      ( i e. b , j e. b |-> ( ( +f ` r ) " ( i X. j ) ) ) >. ,
+            <. ( .r ` ndx ) , ( i e. b , j e. b |->
+              ( ( RSpan ` r ) ` ( ( +f ` ( mulGrp ` r ) ) " ( i X. j ) ) ) ) >.
+     } u. { <. ( TopSet ` ndx ) , ran ( i e. b |->
+                ( b \ { j e. ( PrmIdeal ` r ) | j C_ i } ) ) >. ,
+            <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ b /\ i C_ j ) } >.
+     } ) ) $.
+  $}
+
+  $( Extend class notation with the spectrum of a ring. $)
+  crspec $a class Spec $.
+
+  $( Define the spectrum of a ring.  (Contributed by Thierry Arnoux,
+     21-Jan-2024.) $)
+  df-rspec $a |- Spec = ( r e. Ring |-> ( ( IDLsrg ` r ) |`s ( PrmIdeal ` r )
+    ) ) $.
+
+
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
   The subring algebra