Theorem Multiset.toFinset_card_eq_one_iff

Modification history

2024-02-15 16:15
Mathlib/Data/Finset/Card.lean
feat: add `Multiset.toFinset_(eq_singleton|card_eq_one)_iff` (#10571)
Added Multiset.toFinset_card_eq_one_iffView on Github →