Theorem continuous_equiv_fun_basis
Modification history
2022-06-03 10:31
src/analysis/normed_space/finite_dimension.lean
feat(topology/algebra/module/finite_dimension): all linear maps from a finite dimensional T2 TVS are continuous (#13460) …
Modified continuous_equiv_fun_basisView on Github →2021-05-10 07:36
src/analysis/normed_space/finite_dimension.lean
refactor(*): bundle `is_basis` (#7496) …
Modified continuous_equiv_fun_basisView on Github →2020-05-14 11:14
src/analysis/normed_space/finite_dimension.lean
chore(linear_algebra/basis): use dot notation, simplify some proofs (#2671)
Modified continuous_equiv_fun_basisView on Github →