Commit 2023-12-04 18:10 6b659391
View on Github →feat(Algebra/Ring/CentroidHom): missing scalar instances (#8742)
This generalizes the ℕ and ℤ actions to arbitrary monoids, and provides various compatibility instances.
The simpNF annotations are no longer needed, as the the smul lemmas are now about general actions, not just nsmul and zsmul which have different simp-normal forms.