mathlib

4c7d95fb - feat(analysis/normed_space/inner_product): reflections API (#8884)

feat(analysis/normed_space/inner_product): reflections API (#8884) Reflections, as isometries of an inner product space, were defined in #8660. In this PR, various elementary lemmas filling out the API: - Lemmas about reflection through a subspace K, of a point which is in (i) K itself; (ii) the orthogonal complement of K. - Lemmas relating the orthogonal projection/reflection on the `submodule.map` of a subspace, with the orthogonal projection/reflection on the original subspace. - Lemma characterizing the reflection in the trivial subspace. Co-authored-by: Scott Morrison <scott@tqft.net>