remove more hypotheses in §Additional definitions for (multivariate) polynomials (#5017)

* remove hypotheses: mplelsfi, selvval

* remove hypotheses in ismhp*, prove sn-base0

ismhp* has more axioms by elbaseov > base0, so sn-base0 is proven to justify the change

* remove hypotheses in psd*

---------

Co-authored-by: avekens <[email protected]>

Author: icecream17

changes-set.txt

@@ -93,6 +93,18 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 23-Sep-25 elfzolem1 [same]      moved from GS's mathbox to main set.mm
+17-Sep-25 psdmul    [same]      Removed unneeded hypothesis
+17-Sep-25 psdvsca   [same]      Removed unneeded hypothesis
+17-Sep-25 psdadd    [same]      Removed unneeded hypothesis
+17-Sep-25 psdmplcl  [same]      Removed unneeded hypothesis
+17-Sep-25 psdcl     [same]      Removed unneeded hypothesis
+17-Sep-25 psdcoef   [same]      Removed unneeded hypotheses
+17-Sep-25 psdval    [same]      Removed unneeded hypotheses
+16-Sep-25 ismhp3    [same]      Removed unneeded hypotheses
+16-Sep-25 ismhp2    [same]      Removed unneeded hypotheses
+16-Sep-25 ismhp     [same]      Removed unneeded hypotheses
+16-Sep-25 selvval   [same]      Removed unneeded hypotheses
+16-Sep-25 mplelsfi  [same]      Removed unused hypothesis
 11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 10-Sep-25 soeq12d   [same]      Moved from SO's mathbox to main set.mm
 10-Sep-25 freq12d   [same]      Moved from SO's mathbox to main set.mm

discouraged

@@ -4719,6 +4719,7 @@
 "df-base" is used by "resvbasOLD".
 "df-base" is used by "rmodislmodOLD".
 "df-base" is used by "slotsbhcdifOLD".
+"df-base" is used by "sn-base0".
 "df-base" is used by "srabaseOLD".
 "df-base" is used by "symgvalstructOLD".
 "df-base" is used by "tngbasOLD".
@@ -16029,7 +16030,7 @@ New usage of "df-aj" is discouraged (1 uses).
 New usage of "df-ass" is discouraged (1 uses).
 New usage of "df-at" is discouraged (2 uses).
 New usage of "df-ba" is discouraged (1 uses).
-New usage of "df-base" is discouraged (31 uses).
+New usage of "df-base" is discouraged (32 uses).
 New usage of "df-bdop" is discouraged (2 uses).
 New usage of "df-bj-1upl" is discouraged (6 uses).
 New usage of "df-bj-2upl" is discouraged (6 uses).
@@ -19375,6 +19376,7 @@ New usage of "smfval" is discouraged (17 uses).
 New usage of "smgrpassOLD" is discouraged (1 uses).
 New usage of "smgrpismgmOLD" is discouraged (1 uses).
 New usage of "smgrpmgm" is discouraged (1 uses).
+New usage of "sn-base0" is discouraged (0 uses).
 New usage of "sn-exelALT" is discouraged (0 uses).
 New usage of "sn-isghm" is discouraged (0 uses).
 New usage of "sn-wcdeq" is discouraged (0 uses).
@@ -21649,6 +21651,7 @@ Proof modification of "slotsbhcdifOLD" is discouraged (96 steps).
 Proof modification of "smgrpassOLD" is discouraged (54 steps).
 Proof modification of "smgrpismgmOLD" is discouraged (22 steps).
 Proof modification of "sn-00id" is discouraged (47 steps).
+Proof modification of "sn-base0" is discouraged (4 steps).
 Proof modification of "sn-exelALT" is discouraged (52 steps).
 Proof modification of "sn-isghm" is discouraged (432 steps).
 Proof modification of "snelpwiOLD" is discouraged (20 steps).