Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes