Theorem GradedMonoid.GradeZero.smul_eq_mul

Modification history