Commit 2025-02-14 08:16 75b995ce

View on Github →

chore(AlgebraicTopology): split SimplexCategory.lean (#21625) We split Mathlib/AlgebraicTopology/SimplexCategory.lean into two files, SimplexCategory/Defs.lean and SimplexCategory/Basic.lean.

  • Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean contains the core definitions and notations needed to define the simplex category, the truncated simplex category, and their respective SmallCategory instances.
  • Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean contains everything else.

Estimated changes

deleted theorem SimplexCategory.Hom.ext'
deleted theorem SimplexCategory.Hom.ext
deleted theorem SimplexCategory.ext
deleted def SimplexCategory.len
deleted theorem SimplexCategory.len_mk
deleted def SimplexCategory.mk
deleted theorem SimplexCategory.mk_len
deleted def SimplexCategory
added theorem SimplexCategory.ext
added theorem SimplexCategory.len_mk
added theorem SimplexCategory.mk_len
added def SimplexCategory