summaryrefslogtreecommitdiff
path: root/Nominal/Helpers/Finset.lean
AgeCommit message (Collapse)Author
2025-10-20Prove nonempty induction on finsetsHannes Schulze