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