Commit 2024-12-19 19:41 220ed18e
View on Github →chore(Fintype): move nonempty_fintype (#20053)
This implication doesn't need the axiom of choice or Fintype.card.
Currently, it depends on Classical.choice
because Fin.fintype depends on it (for no good reason).