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.

Estimated changes