Theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul_of_isSMulRegular

Modification history