Theorem TypeVec.dropFun_diag

Modification history

2025-10-07 17:36
Mathlib/Data/TypeVec.lean
chore(Data): golf entire `equivFunOnFintype_single`, `predAbove_right_zero`, `snoc_zero` and more using `rfl` (#28561)
Modified TypeVec.dropFun_diagView on Github →
2023-01-17 19:22
Mathlib/Data/TypeVec.lean
feat: port Data.Typevec (#891) …
Added TypeVec.dropFun_diagView on Github →