Commit 2026-09-02 11:46 8571709f

refactor(AlgebraicTopology): redefine the topological simplex using StdSimplex instead of stdSimplex (#42181) Before #28893, the topological simplex (used for the definition of singular homology) was defined as a subtype of Fin (n + 1) → ℝ≥0 which did not interact well with the convexity API which at the time required working with subtypes of vector spaces. Since #28893, we relied on stdSimplex which was a subtype of Fin (n + 1) → ℝ in order to use the convexity API. Since #31984, the convexity API allows to work with convex spaces not necessarily embedded in vector spaces and we have the new definition of StdSimplex, on which a topology was set up in #42131. This PR deprecates stdSimplex in favour of StdSimplex.