mathlib

f68c936c - feat(analysis/normed_space/real_inner_product): orthogonal subspace lemmas (#4152)