Theorem Subring.toSubsemiring_lt_toSubsemiring

Modification history