Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.nonzero_mem_of_bot_lt

Modification history

2021-10-29 01:24
src/algebra/module/submodule_lattice.lean
chore(algebra/module/submodule_lattice): lemmas about the trivial submodule (#10022) …
Modified submodule.nonzero_mem_of_bot_ltView on Github →
2021-03-19 14:35
src/algebra/module/submodule_lattice.lean
refactor(linear_algebra/basic): move the lattice structure to its own file (#6767) …
Modified submodule.nonzero_mem_of_bot_ltView on Github →
2020-08-26 14:45
src/linear_algebra/basic.lean
feat(ring_theory/noetherian): maximal among set iff Noetherian (#3846) …
Added submodule.nonzero_mem_of_bot_ltView on Github →