Simplicial homology

Stream: new members

[Ruxandra Icleanu]

Hi, I was wondering if there are any projects (or code already in mathlib) on simplicial homology. (For a start, I managed to find the definition of a simplicial complex, but not of an oriented one).

[Joël Riou]

Various people have code for simplicial complexes (not so much is in mathlib though).
We also have definitions for the homology of a simplicial set and the singular homology of a topological space https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicTopology/SingularHomology/Basic.html