Theorem mulRight_bijective₀

Modification history