Commit 2024-10-08 23:23 9341c08e

feat: add Normed instances for SeparationQuotient (#17452) We already have the corresponding metric spaces structures in MetricSpace.Basic. This adds Algebra, NormOneClass, Normed(Add)CommGroup, (Nonunital)Normed(Comm)Ring, NormedSpace, and NormedAlgebra instances. The slightly heavy imports here can be blamed on Topology.Algebra.SeparationQuotient importing LinearAlgebra.Basis.VectorSpace for the final 50-100 lines of the file. Moving this to a new file would cut the chain, as would generalizing it to work in free modules (continuing from #17560), assuming it actually holds there.