mathlib3

52d7570d - chore(data/fintype/basic): don't reimplement finset.map (#17460)