37 theorems from metamath set.mm. If this does not match any format or (future) PR specs let me know - just felt like it was too much work to not contribute it.
I treat mathboxes from users that are in some sense not part of the "official" set.mm library as external libraries even though they're in the same file, which seems like a good convention since they may depend on the non-mathbox part, but not the other way around.
37 theorems from metamath set.mm. If this does not match any format or (future) PR specs let me know - just felt like it was too much work to not contribute it.
I treat mathboxes from users that are in some sense not part of the "official" set.mm library as external libraries even though they're in the same file, which seems like a good convention since they may depend on the non-mathbox part, but not the other way around.