Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-09 12:48 a5f32d27

View on Github →

feat(data/encodable): port countable choice from Lean2

Estimated changes

Modified data/encodable.lean

added theorem encodable.axiom_of_choice

added def encodable.choose

added theorem encodable.choose_spec

added def encodable.pn

added theorem encodable.skolem

added def quot.encodable_quotient

added def quot.rep

added theorem quot.rep_spec