Commit 2024-06-16 10:23 895010aa

View on Github →

feat: 1 ≤ s.card ↔ s.Nonempty (#13821) This shows up when normalising complicated expressions. From LeanAPAP

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_pos

added theorem Finset.one_le_card

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

added theorem Equiv.Perm.support_cycleOf_nonempty