Theorem SimplexCategory.eq_σ_comp_of_not_injective'

Modification history

2025-07-27 16:19

Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

style: use simplex notation (`⦋n⦌`) where possible (#25322) …

Modified SimplexCategory.eq_σ_comp_of_not_injective'View on Github →

2023-04-06 10:57

Mathlib/AlgebraicTopology/SimplexCategory.lean

feat: port AlgebraicTopology.SimplexCategory (#3286)

Added SimplexCategory.eq_σ_comp_of_not_injective'View on Github →