Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-08 18:51 dcb8576b

View on Github →

chore(data/finset/basic): trivial simp lemmas (#4950)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.insert_nonempty

modified theorem finset.singleton_nonempty