Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-18 04:03 d19f7bc6

View on Github →

feat(analysis/normed_space/finite_dimension): finite-dimensional spaces on complete fields (#1687)

  • feat(analysis/normed_space/finite_dimension): equivalence of norms, continuity of linear maps
  • improve doc
  • cleanup
  • cleanup
  • Update src/data/equiv/basic.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • exact_mod_cast, remove classical
  • unfreezeI
  • remove typeclass assumption
  • Update src/analysis/normed_space/finite_dimension.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/linear_algebra/basic.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/linear_algebra/finite_dimensional.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • cleanup

Estimated changes