mathlib
5cbe3c4f - chore(data/finset/powerset): generalize powerset_len_nonempty (#16429)

Commit
3 years ago
chore(data/finset/powerset): generalize powerset_len_nonempty (#16429) `powerset_len_nonempty` holds for `n ≤ s.card`.
Author
Parents
Loading