Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 10:23 3dbd6809

View on Github →

feat(algebraic_topology/dold_kan): construction of an idempotent endomorphism (#15950) In this PR, we pass to the limit in order to obtain the endomorphism P_infty : K[X] ⟶ K[X] of the alternating face map complex. In the case of abelian categories, it shall be the projection on the normalized subcomplex, with kernel the degenerate subcomplex.

Estimated changes