Mathlib v3 is deprecated. Go to Mathlib v4

Theorem encodable.axiom_of_choice

Modification history

2017-09-09 12:48
data/encodable.lean
feat(data/encodable): port countable choice from Lean2
Added encodable.axiom_of_choiceView on Github →