Commit 2021-04-20 00:10 3ad4dabf
View on Github →chore(algebra/*): add back nat_algebra_subsingleton and add_comm_monoid.nat_semimodule.subsingleton (#7263) As suggested in https://github.com/leanprover-community/mathlib/pull/7084#discussion_r613195167. Even if we now have a design solution that makes this unnecessary, it still feels like a result worth stating.