Theorem Fin.snoc_injective_of_injective

Modification history

2025-05-16 03:37
Mathlib/Data/Fin/Tuple/Basic.lean
feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types (#24167) …
Added Fin.snoc_injective_of_injectiveView on Github →