Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-07 23:23 ed4882b1

View on Github →

chore(data/finset/basic): generalize finset.nonempty_mk_coe to nonempty_mk (#16399)

Estimated changes

added theorem finset.nonempty_mk
deleted theorem finset.nonempty_mk_coe