Theorem Finset.mem_cons_of_mem

Modification history

2024-11-11 13:54

Mathlib/Data/Finset/Basic.lean

chore(Data/Finset): split `Basic.lean` into many smaller files (#18610) …

Modified Finset.mem_cons_of_mem View on Github →

2024-03-12 10:00

Mathlib/Data/Finset/Basic.lean

feat: `cons` lemmas for `Finset.noncommProd` (#11194) …

Added Finset.mem_cons_of_mem View on Github →