Theorem Finset.exists_eq_insert_iff

Modification history

2026-04-27 15:18

Mathlib/Data/Finset/Card.lean

chore(Data/Finset/Card): use section variables rather than fresh arguments in three lemmas (#37796)

Modified Finset.exists_eq_insert_iff View on Github →

2023-01-16 16:20

Mathlib/Data/Finset/Card.lean

feat: port Data.Finset.Card (#1589)

Added Finset.exists_eq_insert_iff View on Github →