From e677cc218c9f3114a5ae7662a3cdd3111f08a5ab Mon Sep 17 00:00:00 2001
From: Jim Kingdon <kingdon@panix.com>
Date: Mon, 6 Jan 2025 12:31:22 -0800
Subject: [PATCH] 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.
---
 iset.mm | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/iset.mm b/iset.mm
index b38eb55cbe..4c5155a378 100644
--- a/iset.mm
+++ b/iset.mm
@@ -149026,6 +149026,17 @@ the additive structure must be abelian (see ~ ringcom ), care must be
       WDXKWEFVTAFVTUJXGKVEZAXGBCHWBLVGAXGBDHWBLVGZVHVIXHVQVRFUHZVSHUHXKVRVSHUHZ
       FUHWIWKQXHXOWHVSVSHWBXLAXGBCFVTKVGXHVSVFVHXHXKWEXPWJFVTXMXNAXGCDHWBLVGVHV
       IVJVKVLBCDWNVTGWBVPWQWPVTUPWSVMVN $.
+
+    iscrngd.c $e |- ( ( ph /\ x e. B /\ y e. B ) ->
+      ( x .x. y ) = ( y .x. x ) ) $.
+    $( Properties that determine a commutative ring.  (Contributed by Mario
+       Carneiro, 7-Jan-2015.) $)
+    iscrngd $p |- ( ph -> R e. CRing ) $=
+      ( crg wcel cmgp cfv ccmn ccrg isringd cbs wceq mgpbasg eqtrd cmulr cplusg
+      eqid syl mgpplusgg ismndd iscmnd iscrng sylanbrc ) AGUBUCZGUDUEZUFUCGUGUC
+      ABCDEFGHIJKLMNOPQRSTUHZABCEHVCAEGUIUEZVCUIUEZJAVBVEVFUJVDVEGVCUBVCUOZVEUO
+      UKUPULZAHGUMUEZVCUNUEZLAVBVIVJUJVDGVIVCUBVGVIUOUQUPULZABCDEHVCIVHVKNORSTU
+      RUAUSGVCVGUTVA $.
   $}