Mathlib v3 is deprecated. Go to Mathlib v4

Def vector_space.dim

Modification history

2021-04-24 15:20
src/linear_algebra/dimension.lean
refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322) …
Deleted vector_space.dimView on Github →
2018-11-05 10:47
linear_algebra/dimension.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Modified vector_space.dimView on Github →
2018-01-15 07:59
algebra/linear_algebra/dimension.lean
feat(data/real): reals from first principles …
Added vector_space.dimView on Github →