Commit 2021-11-17 09:02 568435cb

chore(analysis/inner_product_space/projection): typeclass inference for completeness (#10357) As of #5408, most lemmas about orthogonal projection onto a subspace K / reflection through a subspace K / orthogonal complement of K which require K to be complete phrase this in terms of complete_space K rather than is_complete K, so that it can be found by typeclass inference. A few still used the old way; this PR completes the switch.