From 1fb12053d9fac83ae2b7097818c1a91a8029a4e8 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 20 May 2025 17:32:53 -0700 Subject: [PATCH 01/21] Add znle to iset.mm Stated as in set.mm. The proof is based on the set.mm proof of znle and the iset.mm proof of znval . --- iset.mm | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/iset.mm b/iset.mm index 7aaf39f82e..ce241d12ff 100644 --- a/iset.mm +++ b/iset.mm @@ -161828,6 +161828,25 @@ According to Wikipedia ("Integer", 25-May-2019, ZVAXLXLYBXLXLXJXJXKXMXNCVATTYCXOYDUWDUWCUWFCTXPXHUVHUVITTYCXQXFYEDBTTWS XRXSXTYA $. $} + + znle.l $e |- .<_ = ( le ` Y ) $. + $( The value of the ` Z/nZ ` structure. It is defined as the quotient ring + ` ZZ / n ZZ ` , with an "artificial" ordering added. (In other words, + ` Z/nZ ` is a _ring_ with an _order_ , but it is not an _ordered ring_ , + which as a term implies that the order is compatible with the ring + operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) + (Revised by AV, 13-Jun-2019.) $) + znle $p |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) ) $= + ( wcel cple cfv cle cvv czring crg cn0 cnx ccom ccnv cop csts eqid fveq2d + co znval wceq a1i csn cqus zringring crsp rspex ax-mp eqeltri snexg fvexg + cqg sylancr eqgex qusex eqeltrid czrh cres zrhex resexg 3syl cxr cxp xrex + xpex lerelxr ssexi coexg sylancl cnvexg syl2anc pleslid setsslid 3eqtr4d + syl ) EUANZGOPZBUBOPCQUCZCUDZUCZUEUFUIZOPZDWJWFGWKOABCWJEFGHIJKLWJUGUJUHD + WGUKWFMULWFBRNZWJRNZWJWLUKWFBSSEUMZAPZVBUIZUNUIZRIWFSTNZWQRNZWRRNUOWFWSWP + RNZWTUOWFARNWORNXAASUPPZRHWSXBRNUOTSUQURUSEUAUTWOARRVAVCWPSTRVDVCWQSTRVEV + CVFZWFWHRNZWIRNZWNWFCRNZQRNXDWFCBVGPZFVHZRKWFWMXGRNXHRNXCBXGRXGUGVIXGFRVJ + VKVFZQVLVLVMVLVLVNVNVOVPVQCQRRVRVSWFXFXEXICRVTWEWHWIRRVRWARWJORBWBWCWAWD + $. $} From af51dae3c219760fcfbb00d4c71f862fb272253b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 20 May 2025 17:34:28 -0700 Subject: [PATCH 02/21] copy znval2 from set.mm to iset.mm --- iset.mm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/iset.mm b/iset.mm index ce241d12ff..ecb288806b 100644 --- a/iset.mm +++ b/iset.mm @@ -161849,6 +161849,23 @@ According to Wikipedia ("Integer", 25-May-2019, $. $} + ${ + $d x E $. $d x K $. $d x y N $. $d x y U $. $d x y Y $. + znval2.s $e |- S = ( RSpan ` ZZring ) $. + znval2.u $e |- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) ) $. + znval2.y $e |- Y = ( Z/nZ ` N ) $. + ${ + znval2.l $e |- .<_ = ( le ` Y ) $. + $( Self-referential expression for the ` Z/nZ ` structure. (Contributed + by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) $) + znval2 $p |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) ) $= + ( cn0 wcel cnx cple cfv cc0 co ccom cop csts eqid czrh wceq cz cfzo cif + cres cle ccnv znval znle opeq2d oveq2d eqtr4d ) DJKZEBLMNZBUANDOUBUCODU + DPUEZUFZUGQUQUHQZRZSPBUOCRZSPABUQURDUPEFGHUQTZUPTZURTUIUNUTUSBSUNCURUOA + BUQCDUPEFGHVAVBIUJUKULUM $. + $} + $} + $( ############################################################################### From 5b7130c910f95b317f7a7e31e95167d5d42e6cc0 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 20 May 2025 22:48:11 -0700 Subject: [PATCH 03/21] Add znbaslemnn to iset.mm This is znbaslem from set.mm with an added hypothesis. The proof is somewhat based on the set.mm proof but needs a lot more set existence steps. --- iset.mm | 23 +++++++++++++++++++++++ mmil.raw.html | 6 ++++++ 2 files changed, 29 insertions(+) diff --git a/iset.mm b/iset.mm index ecb288806b..4543ad9aa1 100644 --- a/iset.mm +++ b/iset.mm @@ -161864,6 +161864,29 @@ According to Wikipedia ("Integer", 25-May-2019, DPUEZUFZUGQUQUHQZRZSPBUOCRZSPABUQURDUPEFGHUQTZUPTZURTUIUNUTUSBSUNCURUOA BUQCDUPEFGHVAVBIUJUKULUM $. $} + + ${ + znbaslem.e $e |- E = Slot ( E ` ndx ) $. + znbaslemnn.nn $e |- ( E ` ndx ) e. NN $. + znbaslem.n $e |- ( E ` ndx ) =/= ( le ` ndx ) $. + $( Lemma for ~ znbas . (Contributed by Mario Carneiro, 14-Jun-2015.) + (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, + 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, + 3-Nov-2024.) $) + znbaslemnn $p |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) ) $= + ( wcel cfv co cvv czring crg cle eqid syl cn0 cnx cple cop csts csn cqg + wceq cqus zringring rspex ax-mp eqeltri snexg fvexg sylancr eqgex qusex + crsp eqeltrid czrh cc0 cz cfzo cif cres ccom ccnv znval cn plendxnn a1i + zrhex resexg cxr xrex lerelxr ssexi coexg sylancl cnvexg syl2anc setsex + cxp xpex syl3anc eqeltrd pleslid slotex ndxslid setsslnid znval2 fveq2d + eqtr4d ) DUALZBCMZBUBUCMZEUCMZUDUENZCMZECMWOBOLZWROLZWPWTUHWOBPPDUFZAMZ + UGNZUINZOGWOPQLZXEOLZXFOLUJWOXGXDOLZXHUJWOAOLXCOLXIAPUSMZOFXGXJOLUJQPUK + ULUMDUAUNXCAOOUOUPXDPQOUQUPXEPQOURUPUTZWOEOLXBWOEBWQBVAMZDVBUHVCVBDVDNV + EZVFZRVGZXNVHZVGZUDUENZOABXNXQDXMEFGHXNSXMSXQSVIWOXAWQVJLZXQOLZXROLXKXS + WOVKVLWOXOOLZXPOLZXTWOXNOLZROLYAWOXLOLZYCWOXAYDXKBXLOXLSVMTXLXMOVNTZRVO + VOWDVOVOVPVPWEVQVRXNROOVSVTWOYCYBYEXNOWATXOXPOOVSWBWQXQBOOVJWCWFWGEUCOW + HWITOWRWQCOBCUBCMIJWJKVKWKWBWOEWSCABWRDEFGHWRSWLWMWN $. + $} $} diff --git a/mmil.raw.html b/mmil.raw.html index 8c66c82c0a..7664768a5e 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12155,6 +12155,12 @@ used in set.mm + + znbaslem + ~ znbaslemnn + adds ` ( E `` ndx ) e. NN ` hypothesis + + relt none From 3af74a03bb8316f862b1bc4c53eb4abae22779af Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Tue, 20 May 2025 23:40:42 -0700 Subject: [PATCH 04/21] Add znbas2 to iset.mm Stated as in set.mm. The proof is the set.mm proof with a small amount of intuitionizing. --- iset.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/iset.mm b/iset.mm index 4543ad9aa1..5b6ec2df1a 100644 --- a/iset.mm +++ b/iset.mm @@ -161887,6 +161887,13 @@ According to Wikipedia ("Integer", 25-May-2019, VOWDVOVOVPVPWEVQVRXNROOVSVTWOYCYBYEXNOWATXOXPOOVSWBWQXQBOOVJWCWFWGEUCOW HWITOWRWQCOBCUBCMIJWJKVKWKWBWOEWSCABWRDEFGHWRSWLWMWN $. $} + + $( The base set of ` Z/nZ ` is the same as the quotient ring it is based + on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, + 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) + znbas2 $p |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) ) $= + ( cbs baseid basendxnn cnx cple cfv plendxnbasendx necomi znbaslemnn ) AB + HCDEFGIJKLMKHMNOP $. $} From d6e9479a26bc44cab1ff92d9aeba6a0500c272b2 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 18:54:32 -0700 Subject: [PATCH 05/21] Add znadd to iset.mm Stated as in set.mm. The proof is the set.mm proof with a small amount of intuitionizing. --- iset.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/iset.mm b/iset.mm index 5b6ec2df1a..e7711e4063 100644 --- a/iset.mm +++ b/iset.mm @@ -161894,6 +161894,13 @@ According to Wikipedia ("Integer", 25-May-2019, znbas2 $p |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) ) $= ( cbs baseid basendxnn cnx cple cfv plendxnbasendx necomi znbaslemnn ) AB HCDEFGIJKLMKHMNOP $. + + $( The additive structure of ` Z/nZ ` is the same as the quotient ring it + is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by + AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) + znadd $p |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) ) $= + ( cplusg plusgid plusgndxnn cnx cple plendxnplusgndx necomi znbaslemnn + cfv ) ABHCDEFGIJKLPKHPMNO $. $} From a5abdfd5b99397332574e0dbafd9ad2e74d7be8b Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 18:57:57 -0700 Subject: [PATCH 06/21] Add znmul to iset.mm Stated as in set.mm. The proof is the set.mm proof, lightly intuitionized. --- iset.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/iset.mm b/iset.mm index e7711e4063..36a09c6ef4 100644 --- a/iset.mm +++ b/iset.mm @@ -161901,6 +161901,13 @@ According to Wikipedia ("Integer", 25-May-2019, znadd $p |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) ) $= ( cplusg plusgid plusgndxnn cnx cple plendxnplusgndx necomi znbaslemnn cfv ) ABHCDEFGIJKLPKHPMNO $. + + $( The multiplicative structure of ` Z/nZ ` is the same as the quotient + ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) + (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) $) + znmul $p |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) ) $= + ( cmulr mulridx cnx cfv cslot wceq cn wcel mulrslid simpri plendxnmulrndx + cple necomi znbaslemnn ) ABHCDEFGIHJHKZLMUBNOPQJSKUBRTUA $. $} From a2091083fb729071c4215400d80bad3271969cd0 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:19:04 -0700 Subject: [PATCH 07/21] add znmul to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 7664768a5e..436baf09f6 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12161,6 +12161,12 @@ adds ` ( E `` ndx ) e. NN ` hypothesis + + znzrh + none + the set.mm proof uses zrhpropd + + relt none From 4249e7ac6523f579caa59afceedf936a2ccb00e7 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:28:42 -0700 Subject: [PATCH 08/21] Add znbas to iset.mm Stated as in set.mm. The proof needs some intuitionizing but is basically the set.mm proof. --- iset.mm | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/iset.mm b/iset.mm index 36a09c6ef4..5e97581b62 100644 --- a/iset.mm +++ b/iset.mm @@ -161910,6 +161910,20 @@ According to Wikipedia ("Integer", 25-May-2019, cple necomi znbaslemnn ) ABHCDEFGIHJHKZLMUBNOPQJSKUBRTUA $. $} + ${ + znbas.s $e |- S = ( RSpan ` ZZring ) $. + znbas.y $e |- Y = ( Z/nZ ` N ) $. + znbas.r $e |- R = ( ZZring ~QG ( S ` { N } ) ) $. + $( The base set of ` Z/nZ ` structure. (Contributed by Mario Carneiro, + 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) $) + znbas $p |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) ) $= + ( cn0 wcel cz czring cqus co cbs cfv cvv crg a1i zringring sylancr qusbas + cqs eqidd wceq zringbas csn crsp rspex ax-mp eqeltri snexg fvexg eqeltrid + cqg eqgex oveq2i znbas2 eqtrd ) CHIZJAUBKALMZNODNOUSAKUTJPQUSUTUCJKNOUDUS + UERUSAKCUFZBOZUNMZPGUSKQIZVBPIZVCPISUSBPIVAPIVEBKUGOZPEVDVFPISQKUHUIUJCHU + KVABPPULTVBKQPUOTUMVDUSSRUABUTCDEAVCKLGUPFUQUR $. + $} + $( ############################################################################### From b3826e7c1ed486b9147165beaaf67775c5825dc6 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:30:02 -0700 Subject: [PATCH 09/21] copy zncrng from set.mm to iset.mm --- iset.mm | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/iset.mm b/iset.mm index 5e97581b62..fc9e375cd1 100644 --- a/iset.mm +++ b/iset.mm @@ -161924,6 +161924,19 @@ According to Wikipedia ("Integer", 25-May-2019, KVABPPULTVBKQPUOTUMVDUSSRUABUTCDEAVCKLGUPFUQUR $. $} + ${ + $d x y N $. $d x y Y $. + zncrng.y $e |- Y = ( Z/nZ ` N ) $. + $( ` Z/nZ ` is a commutative ring. (Contributed by Mario Carneiro, + 15-Jun-2015.) $) + zncrng $p |- ( N e. NN0 -> Y e. CRing ) $= + ( vx vy cn0 wcel czring csn crsp cfv cqg co cqus ccrg cplusg oveqdr cmulr + eqid cv cz nn0z zncrng2 syl cbs eqidd znbas2 znadd znmul crngpropd mpbid + wa ) AFGZHHAIHJKZKLMNMZOGZBOGUMAUAGUPAUBUNUOAUNSZUOSZUCUDUMDEUOUEKZUOBUMU + SUFUNUOABUQURCUGUMDTUSGETUSGULZDEUOPKBPKUNUOABUQURCUHQUMUTDEUORKBRKUNUOAB + UQURCUIQUJUK $. + $} + $( ############################################################################### From f7665f48692ced51303e2706ea18a1e7d660e14d Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:37:39 -0700 Subject: [PATCH 10/21] add znzrh2 to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 436baf09f6..a608d4735b 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12167,6 +12167,12 @@ the set.mm proof uses zrhpropd + + znzrh2 + none + the set.mm proof uses znzrh + + relt none From f2ba31b3c6bf18687a249b1d342a369e3ec47b1f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:39:06 -0700 Subject: [PATCH 11/21] add znzrhval to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index a608d4735b..2c0a127129 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12173,6 +12173,12 @@ the set.mm proof uses znzrh + + znzrhval + none + the set.mm proof uses znzrh2 + + relt none From 1ca7a746782b0cf175447696a883963d826b85d9 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:50:07 -0700 Subject: [PATCH 12/21] add zncyg to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 2c0a127129..f5e6b2ba49 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12179,6 +12179,12 @@ the set.mm proof uses znzrh2 + + zncyg + none + the set.mm proof uses CycGrp , iscyg , and znzrhfo + + relt none From 7ceefbe49e5219d7643627092896debebf92815a Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 19:54:36 -0700 Subject: [PATCH 13/21] add zndvds to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index f5e6b2ba49..ed2b5166fb 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12185,6 +12185,12 @@ the set.mm proof uses CycGrp , iscyg , and znzrhfo + + zndvds + none + the set.mm proof uses znzrhval + + relt none From 788d279b218113c9ddea4ae5c24e82da3256f823 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 20:39:34 -0700 Subject: [PATCH 14/21] add zndvds0 to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index ed2b5166fb..f6e2a1b46d 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12191,6 +12191,12 @@ the set.mm proof uses znzrhval + + zndvds0 + none + the set.mm proof uses zndvds + + relt none From 81c3cbe08b26d747f6c0ac6f7c44f781458cf00e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 20:51:32 -0700 Subject: [PATCH 15/21] add znzrhfo and znf1o to mmil.html --- mmil.raw.html | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index f6e2a1b46d..85f0d6c5ed 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12179,6 +12179,12 @@ the set.mm proof uses znzrh2 + + znzrhfo + none + the set.mm proof uses znzrh2 + + zncyg none @@ -12197,6 +12203,12 @@ the set.mm proof uses zndvds + + znf1o + none + the set.mm proof uses keephyp and znzrhfo + + relt none From 14ebced6cfe54e46a6926640a7a2143d0a4e1501 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Wed, 21 May 2025 20:55:00 -0700 Subject: [PATCH 16/21] add zzngim to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 85f0d6c5ed..8e480f5978 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12209,6 +12209,13 @@ the set.mm proof uses keephyp and znzrhfo + + zzngim + none + the set.mm proof uses znzrhfo , znf1o , and + isgim + + relt none From 793851f8ed97e709ada97a2bd5bdfecb61e110db Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 22 May 2025 08:19:24 -0700 Subject: [PATCH 17/21] Add znle2 to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 8e480f5978..36e47f1079 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12216,6 +12216,12 @@ isgim + + znle2 + none + the set.mm proof uses znzrh + + relt none From b74d9ba656ac28c2a1c92785ec6cbc6c8cc38aad Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 22 May 2025 08:25:02 -0700 Subject: [PATCH 18/21] add znleval to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 36e47f1079..28175893c4 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12222,6 +12222,12 @@ the set.mm proof uses znzrh + + znleval + none + the set.mm proof uses znle2 + + relt none From 3308c7f2919f597e48437c0ad992c85e5ea22f57 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 22 May 2025 08:25:54 -0700 Subject: [PATCH 19/21] add znleval2 to mmil.html --- mmil.raw.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mmil.raw.html b/mmil.raw.html index 28175893c4..1e576f3431 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12223,7 +12223,7 @@ - znleval + znleval , znleval2 none the set.mm proof uses znle2 From 3face5ada3214b2bf5bb374ac288d71a7d87a154 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 22 May 2025 08:31:28 -0700 Subject: [PATCH 20/21] add zntoslem and zntos to mmil.html --- mmil.raw.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 1e576f3431..2b2380d99f 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12228,6 +12228,13 @@ the set.mm proof uses znle2 + + zntoslem , zntos + none + the set.mm proof uses keephyp , znleval2 , istos , + and isposd + + relt none From 72e07f883554d9eec5b51328e3bae8f93009466f Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 22 May 2025 16:51:29 -0700 Subject: [PATCH 21/21] Add znhash to mmil.html --- mmil.raw.html | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mmil.raw.html b/mmil.raw.html index 2b2380d99f..2a04d51273 100644 --- a/mmil.raw.html +++ b/mmil.raw.html @@ -12235,6 +12235,12 @@ and isposd + + znhash + none + the set.mm proof uses znf1o + + relt none