Commit 2023-12-04 13:54 19096ec3

View on Github →

chore(NormedSpace/Complemented): review API (#8596)

  • use And instead of Exists;
  • move lemmas from Subspace to Submodule namespace;
  • rename some lemmas to enable dot notation;
  • add ClosedComplemented.exists_submodule_equiv_prod.

Estimated changes