Theorem Monoid.PushoutI.NormalWord.ext_smul

Modification history