Mathlib Changelog
v3
Changelog
About
Github
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_bot
View 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_bot
View 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_bot
View on Github →