Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-13 02:46 f3187269

View on Github →

feat(data/multiset/basic): multiset.coe_eq_singleton (#15910)

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.coe_eq_singleton

modified theorem multiset.coe_singleton

added theorem multiset.to_list_eq_singleton_iff

added theorem multiset.to_list_singleton