Theorem AList.empty_lookupFinsupp

Modification history

2025-10-07 17:36
Mathlib/Data/Finsupp/AList.lean
chore(Data): golf entire `equivFunOnFintype_single`, `predAbove_right_zero`, `snoc_zero` and more using `rfl` (#28561)
Modified AList.empty_lookupFinsuppView on Github →
2023-02-02 05:25
Mathlib/Data/Finsupp/AList.lean
feat Port/Data.Finsupp.AList (#1991) …
Added AList.empty_lookupFinsuppView on Github →