Intuitionize Ring and CRing up until iscrngd (#4540)

* Add Ring and CRing to iset.mm

This is the syntax , df-ring , and df-cring .  Copied without change
from set.mm.

* Add isring to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Copy ringgrp and ringmgp from set.mm to iset.mm

* copy iscrng and crngmgp from set.mm to iset.mm

* copy ringgrpd and ringmnd from set.mm to iset.mm

* copy ringmgm and crngring from set.mm to iset.mm

* copy crngringd and crnggrpd from set.mm to iset.mm

* copy mgpf from set.mm to iset.mm

* Add ringcl to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add crngcom to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add iscrng2 to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add ringass to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add ringideu to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Rename ringi to ringdilem in set.mm

* copy ring distributivity theorems to iset.mm

This is ringdilem , ringdi , and ringdir .  Copied without change from
set.mm.

* Add ringidcl to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy ring0cl from set.mm to iset.mm

* Add ringlidm and ringridm to iset.mm

Includes lemma ringidmlem , which is stated as in set.mm.  Its proof
needs some intuitionizing but is basically the set.mm proof.

ringlidm and ringridm are copied without change from set.mm.

* Add isringid to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy ringid from set.mm to iset.mm

* copy ringadd2 from set.mm to iset.mm

* copy rngo2times from set.mm to iset.mm

* add ringidss to mmil.html

* copy ringacl from set.mm to iset.mm

* Add ringcom to iset.mm

Copied from set.mm, with the only change being to the comment, to remove
a reference to a theorem iset.mm doesn't have yet.

* copy ringabl and ringcmn from set.mm to iset.mm

* Add ringpropd to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* Add crngpropd to iset.mm

Stated as in set.mm.  The proof needs some intuitionizing but is
basically the set.mm proof.

* copy ringprop from set.mm to iset.mm

* Add isringd to iset.mm

Stated as in set.mm.  The proof needs a small amount of intuitionizing
but is basically the set.mm proof.

* Add iscrngd to iset.mm

Stated as in set.mm.  The proof needs a little bit of intuitionizing but
is basically the set.mm proof.

changes-set.txt

@@ -92,8 +92,9 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
- 5-Jan-26 nfrexd    nfrexdw     consistent with nfraldw
- 5-Jan-26 nfrex     nfrexw      consistent with nfralw
+ 7-Jan-25 ringi     ringdilem
+ 5-Jan-25 nfrexd    nfrexdw     consistent with nfraldw
+ 5-Jan-25 nfrex     nfrexw      consistent with nfralw
  4-Jan-25 smorndom  smocdmdom
  4-Jan-25 ralimda   ---         obsolete - use ralimdaa instead
  3-Jan-25 srgi      srgdilem