Theorem Monoid.CoprodI.Word.smul_eq_of_smul

Modification history