Commit 2025-02-03 07:17 600654aa

View on Github →

feat(Order): Fin.succAboveOrderIso (#21303) This PR introduces the order isomorphism Fin.succAboveOrderIso i : Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2))) for i : Fin (n + 2).

Estimated changes