Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-29 19:37 505c32f5

View on Github →

feat(analysis/normed_space/inner_product): the orthogonal projection is self adjoint (#8116)

Estimated changes