Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.insert_val_of_not_mem

Modification history

2020-10-13 19:48

src/data/finset/basic.lean

chore(multiset): dedicated notation for multiset.cons (#4600)

Modified finset.insert_val_of_not_mem View on Github →

2018-04-24 22:18

data/finset.lean

fix(*): update to lean

Added finset.insert_val_of_not_mem View on Github →