Commit 2025-07-27 16:19 56dfd717

View on Github →

style: use simplex notation (⦋n⦌) where possible (#25322) StandardSimplex.mk n is replaced with ⦋n⦌ where possible (except in notation and macros, which are left untouched). This includes opening Simplicial (scoped) in two files. Also, outdated and unused local notation [n] for StandardSimplex.mk n is removed.

Estimated changes

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/AlgebraicTopology/MooreComplex.lean

modified def AlgebraicTopology.NormalizedMooreComplex.objX

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

modified theorem SimplexCategory.eq_comp_δ_of_not_surjective'

modified theorem SimplexCategory.eq_comp_δ_of_not_surjective

modified theorem SimplexCategory.eq_δ_of_mono

modified theorem SimplexCategory.eq_σ_comp_of_not_injective'

modified theorem SimplexCategory.eq_σ_comp_of_not_injective

modified theorem SimplexCategory.eq_σ_of_epi

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

modified def SSet.stdSimplex.isoOfRepresentableBy

modified theorem SSet.stdSimplex.objEquiv_symm_apply