Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-30 00:36 ddbb8138

View on Github →

feat(data/fintype): finite choices, computably

Estimated changes

Modified data/fintype.lean

added def quotient.fin_choice

added def quotient.fin_choice_aux

added theorem quotient.fin_choice_aux_eq

added theorem quotient.fin_choice_eq

Modified data/quot.lean

added theorem quotient.choice_eq