Theorem Fin.snoc_left_injective

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.snoc_left_injective View on Github →