Commit 2023-12-19 00:17 8d91b8e7

View on Github →

feat: Finset/Multiset.powersetCard 1 (#9137) for [#9130](https://github.com/leanprover-community/mathlib4/pull/9130/files#r1429368677)

Estimated changes

Modified Mathlib/Data/Finset/Powerset.lean

added theorem Finset.powersetCard_one

modified theorem Finset.powersetCard_zero

Modified Mathlib/Data/List/Sublists.lean

added theorem List.sublistsLen_one

Modified Mathlib/Data/Multiset/Powerset.lean

added theorem Multiset.powersetCard_one