mathlib

4ce2a5f1 - chore(algebra/module/submodule_lattice): lemmas about the trivial submodule (#10022)

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.