Theorem SSet.prodStdSimplex.nonDegenerateEquiv₁_fst

Modification history

2026-09-07 10:03

Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

feat(AlgebraicTopology): filtration of `Δ[p] ⊗ Δ[1]` (#41655) …

Deleted SSet.prodStdSimplex.nonDegenerateEquiv₁_fst View on Github →

2026-03-26 08:53

Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in `Δ[n] ⊗ Δ[1]` (#37186)

Added SSet.prodStdSimplex.nonDegenerateEquiv₁_fst View on Github →