Misc. Algebra (#4675)

* Misc. algebra * Formatting * Wording * Shorten `ressbasss` * Rename eqimss2d > eqimsscd
metamath · Feb 28, 2025 · 300fb4d · 300fb4d
1 parent b231bba
commit 300fb4d
Show file tree

Hide file tree

Showing 3 changed files with 456 additions and 166 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -86,6 +86,20 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 27-Feb-25 elnelall  pm2.24nel
+25-Feb-25 eqimssd   [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 eqimss2d  eqimsscd    Moved from SN's mathbox to main set.mm
+25-Feb-25 hashfundm [same]      Moved from BT's mathbox to main set.mm
+25-Feb-25 hashf1dmrn [same]     Moved from BT's mathbox to main set.mm
+25-Feb-25 ressbasssg [same]     Moved from SN's mathbox to main set.mm
+25-Feb-25 ressbasss2 [same]     Moved from SN's mathbox to main set.mm
+25-Feb-25 resrhm2b  [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 sdrgrcl   [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 sdrgdrng  [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 sdrgsubrg [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 sdrgbas   [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 sdrgunit  [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 imadrhmcl [same]      Moved from SN's mathbox to main set.mm
+25-Feb-25 lmhmlvec  [same]      Moved from SN's mathbox to main set.mm
 24-Feb-25 naddid1   naddrid
 24-Feb-25 naddid2   naddlid
 24-Feb-25 mulid1    mulrid

diff --git a/discouraged b/discouraged
@@ -18820,6 +18820,7 @@ New usage of "rescbasOLD" is discouraged (0 uses).
 New usage of "resccoOLD" is discouraged (0 uses).
 New usage of "resfunexgALT" is discouraged (0 uses).
 New usage of "ressbasOLD" is discouraged (0 uses).
+New usage of "ressbasssOLD" is discouraged (0 uses).
 New usage of "resslemOLD" is discouraged (0 uses).
 New usage of "ressval3dOLD" is discouraged (0 uses).
 New usage of "resvbasOLD" is discouraged (0 uses).
@@ -21233,6 +21234,7 @@ Proof modification of "rescbasOLD" is discouraged (106 steps).
 Proof modification of "resccoOLD" is discouraged (115 steps).
 Proof modification of "resfunexgALT" is discouraged (76 steps).
 Proof modification of "ressbasOLD" is discouraged (197 steps).
+Proof modification of "ressbasssOLD" is discouraged (61 steps).
 Proof modification of "resslemOLD" is discouraged (167 steps).
 Proof modification of "ressval3dOLD" is discouraged (285 steps).
 Proof modification of "resvbasOLD" is discouraged (17 steps).