Commit 2025-04-23 13:25 a6d9f970

View on Github →

chore(AlgebraicTopology/ExtraDegeneracy): use Matrix.vecCons (#24199) Cherry-picked from #24196

Estimated changes

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

deleted theorem SSet.Augmented.StandardSimplex.shiftFun_0

added theorem SSet.Augmented.StandardSimplex.shiftFun_zero