Theorem SSet.Truncated.Edge.id_tensor_id

Modification history

2025-12-26 18:30
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
feat(AlgebraicTopology): prerequisites for the commutation of `HomotopyCategory` with binary products (#33201)
Added SSet.Truncated.Edge.id_tensor_idView on Github →