Commit 2024-02-15 16:15 51f04865

View on Github →

feat: add Multiset.toFinset_(eq_singleton|card_eq_one)_iff (#10571)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Multiset.toFinset_eq_singleton_iff

Modified Mathlib/Data/Finset/Card.lean

added theorem Multiset.toFinset_card_eq_one_iff