Commit 2024-09-29 19:04 5a3902a4
View on Github →chore(Topology/Category): fix imports in TopCat.Basic (#17258)
A new file TopCat.Sphere is added so as to remove the import to Analysis.InnerProductSpace.PiL2 that was added to the file Topology.Category.TopCat.Basic in PR #12502.