Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-23 14:30 bd81d555

View on Github →

feat(data/finsupp): add lemmas about single (#9894) These are subset versions of the four lemmas related to support_eq_singleton.

Estimated changes