Commit 2023-12-04 13:54 19096ec3
View on Github →chore(NormedSpace/Complemented): review API (#8596)
- use
And
instead ofExists
; - move lemmas from
Subspace
toSubmodule
namespace; - rename some lemmas to enable dot notation;
- add
ClosedComplemented.exists_submodule_equiv_prod
.