search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

fsuppssind #4050

Closed icecream17 closed 3 weeks ago

icecream17 commented 1 month ago

moved 3 5 theorems to main and shorten proofs automatically

otherwise mathbox

--comment I was going to use fsuppssind to prove mhpmuldeg and mhppwdeg (currently commented out), but then I noticed df-mdeg's proofs, whose way of proving is probably better... So unfortunately, proving this theorem is mostly for nothing.

icecream17 commented 1 month ago

since I wont be able to edit this for a while and there will be merge conflicts, temporarily setting this to draft to give precedence to other prs

edit: resolved

tirix commented 1 month ago

The changes look fine to me, the errors come from missing $d disjoint variable restrictions.

tirix commented 3 weeks ago

Are we good to merge this PR ? @avekens