Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-26 08:53
a17cb031
View on Github →
feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in
Δ[n] ⊗ Δ[1]
(
#37186
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean
added
theorem
SSet.prodStdSimplex.nonDegenerateEquiv₁_fst
added
theorem
SSet.prodStdSimplex.nonDegenerateEquiv₁_snd