mathlib

d7859726 - refactor(data/fintype/basic): move fin_choice to a new file (#18337)

refactor(data/fintype/basic): move fin_choice to a new file (#18337) There is a refactor in the works for these definitions; it will be easier to review and port the refactor if we move this all to a new file first and just forward-port the deletion.