mathlib

3ad4dabf - chore(algebra/*): add back nat_algebra_subsingleton and add_comm_monoid.nat_semimodule.subsingleton (#7263)

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.