Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes