Theorem Subsemiring.mk'_toSubmonoid

Modification history