mathlib

ed98c07f - feat(algebraic_topology/dold_kan): a few basic lemmas and a property of P_infty (#17538)

feat(algebraic_topology/dold_kan): a few basic lemmas and a property of P_infty (#17538) This PR introduces some very basic lemmas for the complement projection `Q` of `P`. We also obtain the lemma `ι_summand_comp_P_infty_eq_zero` which states that in a given degree, `P_infty` vanishes on all the summands of a split simplicial object except one.