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