Theorem AddCommGroup.smul_top_eq_top_of_divisibleBy_int

Modification history