mathlib

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