mathlib3

35f2789c - chore(algebra/module/basic): add `subsingleton (semimodule ℕ M)` (#5396)

chore(algebra/module/basic): add `subsingleton (semimodule ℕ M)` (#5396) This can be used to resolve diamonds between different `semimodule ℕ` instances. The implementation is copied from the `subsingleton (module ℤ M)` instance.