Theorem Fin.ofFn_take_eq_take_ofFn

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