mathlib3

aa730c63 - feat(linear_algebra): a module has a unique submodule iff it has a unique element (#6281)