mathlib

7cf0a29d - feat(analysis/normed_space/inner_product): consequences of characterization of orthogonal projection (#5558)

feat(analysis/normed_space/inner_product): consequences of characterization of orthogonal projection (#5558) Reverse order of equality in the lemma `eq_orthogonal_projection_of_mem_of_inner_eq_zero`. Add some variants. Also add three consequences: - the orthogonal projection onto `K` of an element of `K` is itself - the orthogonal projection onto `K` of an element of `Kᗮ` is zero - for a submodule `K` of an inner product space, the sum of the orthogonal projections onto `K` and `Kᗮ` is the identity. Reverse order of `iff` in the lemma `submodule.eq_top_iff_orthogonal_eq_bot`, and rename to `submodule.orthogonal_eq_bot_iff`.