Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_mem_ne_zero_of_ne_bot

Modification history

2021-10-29 01:24
src/linear_algebra/dimension.lean
chore(algebra/module/submodule_lattice): lemmas about the trivial submodule (#10022) …
Deleted exists_mem_ne_zero_of_ne_botView on Github →
2019-10-10 11:14
src/linear_algebra/dimension.lean
chore(linear_algebra): rename type variables (#1521) …
Modified exists_mem_ne_zero_of_ne_botView on Github →
2019-03-26 18:22
src/linear_algebra/dimension.lean
feat(linear_algebra/dimension): add exists_mem_ne_zero_of_dim_pos
Added exists_mem_ne_zero_of_ne_botView on Github →