Theorem Finset.one_le_card

Modification history

2024-10-17 15:41

Mathlib/Data/Finset/Card.lean

feat: `#s` as notation for `Finset.card s` (#17646) …

Modified Finset.one_le_card View on Github →

2024-06-16 10:23

Mathlib/Data/Finset/Card.lean

feat: `1 ≤ s.card ↔ s.Nonempty` (#13821) …

Added Finset.one_le_card View on Github →