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.