Commit 2024-05-30 05:34 5f2f1f73

View on Github →

refactor: split Fin.succAboveEmb into an Embedding and an OrderEmbedding (#13341)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Data/Fin/OrderHom.lean

added theorem Fin.coe_succAboveEmb

modified def Fin.succAboveEmb

added def Fin.succAboveOrderEmb

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Logic/Equiv/Fin.lean