Theorem Fin.take_one

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_oneView on Github →