Commit 2020-12-17 16:32 35f2789c
View on Github →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.