Theorem Fin.get_take_ofFn_eq_take_comp_cast

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