Commit 2025-03-13 10:26 eaf100ac

chore(Data/Fintype): process porting notes (#22876) One regression is that induction using Fintype.induction_empty_option does not work any more (presumably since we do induction on ɑ but also require a Fintype ɑ argument). Otherwise most of these are uninteresting.