Def SSet.Truncated.Edge.CompStruct.idCompId

Modification history

2025-12-26 18:30

Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean

feat(AlgebraicTopology): prerequisites for the commutation of `HomotopyCategory` with binary products (#33201)

Added SSet.Truncated.Edge.CompStruct.idCompId View on Github →