Theorem AlgebraicTopology.DoldKan.PInfty_f_0

Modification history

2026-04-30 19:12
Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
chore(Algebra/Homology/HomologicalComplex): make CochainComplex.of and ChainComplex.of abbrevs (#38661) …
Modified AlgebraicTopology.DoldKan.PInfty_f_0View on Github →
2025-02-08 20:13
Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
feat(AlgebraicTopology): notations X _⦋n⦌ and X ^⦋n⦌ for (co)simplicial objects (#21581) …
Modified AlgebraicTopology.DoldKan.PInfty_f_0View on Github →
2023-04-20 17:11
Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
feat: port AlgebraicTopology.DoldKan.PInfty (#3539)
Added AlgebraicTopology.DoldKan.PInfty_f_0View on Github →