Theorem Fin.take_succ_eq_snoc

Modification history

2024-10-31 00:24
Mathlib/Data/Fin/Tuple/Take.lean
feat(Data/Fin/Tuple): Define `Fin.take` and initial theorems (#17196) …
Added Fin.take_succ_eq_snocView on Github →