Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-11 22:08 8cfa8363

View on Github →

feat(analysis/inner_product_space/l2_space): if K is a complete submodule then E is the Hilbert sum of K and Kᗮ (#15792)

Estimated changes