Commit 2025-10-17 12:35 5a6cfc3c

View on Github →

fix: Improve definition of SimplexCategoryGenRel.IsAdmissible (#30586) Give SimplexCategoryGenRel.IsAdmissible an inductive definition equivalent to its prior definition.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

modified theorem SimplexCategoryGenRel.IsAdmissible.cons

modified def SimplexCategoryGenRel.IsAdmissible.getElemAsFin

added theorem SimplexCategoryGenRel.IsAdmissible.getElem_lt

modified def SimplexCategoryGenRel.IsAdmissible.head

modified theorem SimplexCategoryGenRel.IsAdmissible.head_lt

added theorem SimplexCategoryGenRel.IsAdmissible.isChain

modified theorem SimplexCategoryGenRel.IsAdmissible.le

added theorem SimplexCategoryGenRel.IsAdmissible.mono

deleted theorem SimplexCategoryGenRel.IsAdmissible.nil

added theorem SimplexCategoryGenRel.IsAdmissible.of_cons

added theorem SimplexCategoryGenRel.IsAdmissible.pairwise

added theorem SimplexCategoryGenRel.IsAdmissible.simplicialEvalσ_succ_getElem

deleted theorem SimplexCategoryGenRel.IsAdmissible.sorted

deleted theorem SimplexCategoryGenRel.IsAdmissible.tail

added inductive SimplexCategoryGenRel.IsAdmissible

deleted def SimplexCategoryGenRel.IsAdmissible

added theorem SimplexCategoryGenRel.isAdmissible_cons_cons_iff

added theorem SimplexCategoryGenRel.isAdmissible_cons_iff

added theorem SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le

added theorem SimplexCategoryGenRel.isAdmissible_iff_pairwise_and_le

added theorem SimplexCategoryGenRel.isAdmissible_of_isChain_of_forall_getElem_le

added theorem SimplexCategoryGenRel.isAdmissible_singleton_iff

added theorem SimplexCategoryGenRel.simplicialEvalσ_of_le_mem

deleted theorem SimplexCategoryGenRel.simplicialEvalσ_of_lt_mem

Modified Mathlib/Data/List/Chain.lean

deleted theorem List.IsChain.cons'

added theorem List.IsChain.cons

added theorem List.IsChain.of_cons

modified theorem List.IsChain.tail

deleted theorem List.isChain_cons'

added theorem List.isChain_cons

Modified Mathlib/Data/List/SplitBy.lean

Modified Mathlib/Data/Nat/Fib/Zeckendorf.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/Order/Height.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

Modified scripts/nolints_prime_decls.txt