mathlib
d908bc0b - chore(data/fintype): drop a `decidable_pred` assumption (#14971)

Commit

3 years ago

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

Author

urkud

Parents