Def SimplexCategoryGenRel.simplicialEvalσ

Modification history

2025-10-04 08:50

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for `P_σ`s (#25736) …

Added SimplexCategoryGenRel.simplicialEvalσ View on Github →