Theorem RCLike.I_mul_re

Modification history