mathlib
5b36c868 - feat(analysis/normed_space/finite_dimension): the determinant is continuous on the space of continuous linear maps (#11526)

Commit
4 years ago
feat(analysis/normed_space/finite_dimension): the determinant is continuous on the space of continuous linear maps (#11526)
Author
Parents
Loading