Commit 2020-07-13 19:35 45477c8f
View on Github →feat(analysis/normed_space/real_inner_product): orthogonal subspaces (#3369) Define the subspace of vectors orthogonal to a given subspace and prove some basic properties of it, building on the existing results about minimizers. This is in preparation for doing similar things in Euclidean geometry (working with the affine subspace through a given point and orthogonal to a given affine subspace, for example).