Theorem SimplexCategoryGenRel.mem_isAdmissible_of_eval_eq_eval_add_one

Modification history

2026-10-31 22:39
Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
chore: remove straightforward redundant theorem hypotheses (#45526) …
Added SimplexCategoryGenRel.mem_isAdmissible_of_eval_eq_eval_add_oneView on Github →