Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.bot_ne_top

Modification history

2021-02-22 14:12
src/linear_algebra/basic.lean
feat(linear_algebra): a module has a unique submodule iff it has a unique element (#6281) …
Deleted submodule.bot_ne_topView on Github →
2020-07-30 07:34
src/linear_algebra/basic.lean
feat(linear_algebra): invariant basis number property (#3560)
Added submodule.bot_ne_topView on Github →