Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-19 02:55 6b93e932

View on Github →

refactor(data/equiv,encodable): refactor/simplify proofs

Estimated changes

Modified data/encodable.lean

modified def encodable.choose

modified theorem encodable.choose_spec

added def encodable.choose_x

deleted def encodable.pn

deleted theorem succ_ne_zero

Modified data/equiv.lean

modified theorem equiv.apply_eq_iff_eq_inverse_apply

modified def equiv.bool_prod_equiv_sum

added def equiv.bool_prod_nat_equiv_nat

modified theorem equiv.coe_fn_symm_mk

added def equiv.equiv_empty

modified def equiv.false_equiv_empty

modified theorem equiv.inverse_apply_apply

modified def equiv.nat_equiv_nat_sum_unit

modified def equiv.nat_prod_nat_equiv_nat

modified def equiv.nat_sum_bool_equiv_nat

added def equiv.nat_sum_nat_equiv_nat

modified def equiv.nat_sum_unit_equiv_nat

added def equiv.option_equiv_sum_unit

added def equiv.prod_equiv_of_equiv_nat

modified def equiv.subtype_equiv_of_subtype

Modified data/fin.lean

Modified data/nat/basic.lean

added theorem nat.bodd_div2_eq

Modified data/option.lean

added theorem option.bind_some

Modified data/set/enumerate.lean

deleted theorem option.bind_some

Modified tactic/interactive.lean