Commit 2020-05-27 08:57 6ee3a47e

View on Github →

chore(data/equiv/basic): simplify some defs, add coe lemmas (#2835) Use functions like prod.map, curry, uncurry, sum.elim, sum.map to define equivalences.

Estimated changes

Modified src/data/equiv/basic.lean

modified theorem equiv.apply_symm_apply

added theorem equiv.coe_prod_comm

added theorem equiv.coe_prod_congr

added theorem equiv.coe_refl

added theorem equiv.coe_trans

modified def equiv.empty_prod

modified theorem equiv.of_bijective_to_fun

modified def equiv.pempty_prod

added theorem equiv.prod_assoc_sym_apply

modified def equiv.prod_comm

deleted theorem equiv.prod_comm_apply

added theorem equiv.prod_comm_symm

modified def equiv.prod_congr

deleted theorem equiv.prod_congr_apply

added theorem equiv.prod_congr_symm

modified def equiv.prod_empty

modified def equiv.prod_pempty

modified def equiv.prod_punit

modified def equiv.psum_equiv_sum

modified def equiv.punit_prod

modified theorem equiv.punit_prod_apply

modified theorem equiv.refl_apply

added theorem equiv.self_comp_symm

modified def equiv.sigma_congr

modified def equiv.sigma_congr_left'

added theorem equiv.sum_comm_apply

deleted theorem equiv.sum_comm_apply_inl

deleted theorem equiv.sum_comm_apply_inr

modified theorem equiv.sum_comm_symm

modified def equiv.sum_congr

added theorem equiv.sum_congr_apply

deleted theorem equiv.sum_congr_apply_inl

deleted theorem equiv.sum_congr_apply_inr

modified theorem equiv.sum_congr_symm

modified def equiv.sum_empty

modified def equiv.sum_pempty

modified theorem equiv.symm_apply_apply

added theorem equiv.symm_comp_self

modified theorem equiv.trans_apply

Modified src/data/equiv/functor.lean

Modified src/data/polynomial.lean

Modified src/data/sum.lean

added theorem sum.map_comp_map

added theorem sum.map_id_id

added theorem sum.map_inl

added theorem sum.map_inr

added theorem sum.map_map