mathlib
6c71874b - feat(analysis/normed_space): complemented subspaces (#2738)

Commit

5 years ago

feat(analysis/normed_space): complemented subspaces (#2738) Define complemented subspaces and prove some basic facts.

Author

urkud

Parents