Commit 2025-03-23 00:48 3067746f

View on Github →

chore: generalize smul_finsum' from Ring to Monoid (#23224) I need it for groups. From FLT

Estimated changes

modified theorem smul_finsum'