Commit 2024-12-20 05:04 97ba55d9

chore(Analysis/InnerProductSpace): split large file (#20046) Split up Analysis.InnerProductSpace.Basic as follows:

• Defs: the definition and the InnerProductSpace.Core stuff
• Basic: general lemmas
• Completion: inner products on completions and separation quotients
• LinearMap: interaction of linear maps with inner products
• Orthonormal: orthonormal families of vectors
• Subspace: subspaces of inner product spaces (including orthogonal families) No code changes, other than deleting one copy of an instance which was declared twice. The file Defs uses ℂ in a notation definition, which is invisible to the tree-shake script, so it needs to have an exception in noshake.json.