Mathlib v3 is deprecated. Go to Mathlib v4

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).

Estimated changes