mathlib

f9c8abe3 - chore(data/finset/basic): a few lemmas about `finset.piecewise` (#4852)