Theorem DFinsupp.support_single_ne_zero

Modification history

2026-05-06 18:10
Mathlib/Data/DFinsupp/Defs.lean
chore(Data/Finsupp): make `support_single` simp (#38860) …
Deleted DFinsupp.support_single_ne_zeroView on Github →
2023-07-12 02:40
Mathlib/Data/DFinsupp/Basic.lean
chore: rename `Dfinsupp` to `DFinsupp` (#5822) …
Added DFinsupp.support_single_ne_zeroView on Github →