Commit 2021-10-29 01:24 4ce2a5f1
View on Github →chore(algebra/module/submodule_lattice): lemmas about the trivial submodule (#10022)
Lemmas about the trivial submodule. Also move an existing lemma exists_mem_ne_zero_of_ne_bot about the trivial submodule from linear_algebra/dimension to algebra/module/submodule_lattice, since it doesn't use any facts about dimension.