Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-13 14:19 e9b077c3

View on Github →

chore(data/equiv): use has_coe_to_fun

Estimated changes

Modified data/equiv.lean

modified theorem equiv.apply_eq_iff_eq

modified theorem equiv.apply_eq_iff_eq_inverse_apply

added theorem equiv.coe_fn_mk

added theorem equiv.coe_fn_symm_mk

modified theorem equiv.comp_apply

modified theorem equiv.eq_of_to_fun_eq

deleted def equiv.fn

modified theorem equiv.id_apply

deleted def equiv.inv

modified theorem equiv.inverse_apply_apply

modified def equiv.subtype_equiv_of_subtype

modified theorem equiv.swap_apply_def

modified theorem equiv.swap_apply_left

modified theorem equiv.swap_apply_of_ne_of_ne

modified theorem equiv.swap_apply_right