Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-06 08:41 d908bc0b

View on Github →

chore(data/fintype): drop a decidable_pred assumption (#14971) OTOH, now the proof depends on classical.choice.

Estimated changes

modified def fintype_of_fintype_ne