Commit 2026-06-05 17:23 24d27c1d

View on Github →

feat(Algebra/Module/LocalizedModule): generalize smul'_mk (#40196) This also moves it higher up the file to make clear it is unrelated to the SMul instance declared next to it. For good measure, I add a missing SMulCommClass instance, even though I didn't need it.

Estimated changes