From 2fa50561c8044fd1f9f28a568e715cbcba8ff6bf Mon Sep 17 00:00:00 2001 From: avekens Date: Sun, 14 Jan 2024 18:48:58 +0100 Subject: [PATCH] BJ's Review remarks --- set.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 87174a424..8694c3341 100644 --- a/set.mm +++ b/set.mm @@ -68489,7 +68489,7 @@ result of an operator (deduction version). (Contributed by Paul $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- - Convert operation laws using setvar variables to class notation + Variable-to-class conversion for operations -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) @@ -180550,7 +180550,7 @@ obviously not a bijection (by Cantor's theorem ~ canth2 ), and in fact BVCVENQUPNVFOVGVHVIVJVK $. $} - $( Obsolete proof of ~ gcdmultiple as of 12-Jan-2024. Extend ~ gcdmultiple + $( Obsolete proof of ~ gcdmultiplez as of 12-Jan-2024. Extend ~ gcdmultiple so ` N ` can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (New usage is discouraged.) (Proof modification is discouraged.) $)