Commit 2019-12-10 16:39 361793a7
View on Github →refactor(linear_algebra/finite_dimensional): universe polymorphism, doc (#1784)
- refactor(linear_algebra/finite_dimensional): universe polymorphism, doc
- docstrings
- improvements
- typo
- Update src/linear_algebra/dimension.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Update src/linear_algebra/finite_dimensional.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Update src/linear_algebra/finite_dimensional.lean Co-Authored-By: Johan Commelin johan@commelin.net
- fix comments
- fix build
- fix build
- remove pp.universe
- keep docstring in sync