Theorem isSMulRegular_quotient_iff_mem_of_smul_mem

Modification history