2025-10-04 08:50
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s (#25736) …
Added SimplexCategoryGenRel.exists_normal_form_P_σ