Theorem CommSemiring.toSemiring_injective

Modification history