Theorem Fin.eq_self_or_eq_succAbove

Modification history

2025-01-21 04:10

Mathlib/Data/Fin/Tuple/Basic.lean

feat(Data/Fin/Tuple/Basic): `snoc` & `insertNth` are injective (#20771) …

Added Fin.eq_self_or_eq_succAbove View on Github →