Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 12:30 e6785319

View on Github →

refactor(data/finset): use generic set notation for finsets

Estimated changes

modified theorem finset.eq_of_mem_singleton
modified theorem finset.eq_of_singleton_eq