Commit 2021-01-27 08:41 20d6b6a7

chore(*): add more simp lemmas, refactor theorems about fintype.sum (#5888)

• finset.prod_sum_elim, finset.sum_sum_elim: use finset.map instead of finset.image;
• add multilinear_map.coe_mk_continuous, finset.order_emb_of_fin_mem, fintype.univ_sum_type, fintype.prod_sum_elim, sum.update_elim_inl, sum.update_elim_inr, sum.update_inl_comp_inl, sum.update_inl_comp_inr, sum.update_inr_comp_inl, sum.update_inr_comp_inr and apply versions of sum.*_comp_* lemmas,
• move some lemmas about function.update from data.set.function to logic.function.basic;
• rename sum.elim_injective to function.injective.sum_elim
• simps lemmas for function.embedding.inl and function.embedding.inr;
• for e : α ≃o β, simplify e.to_equiv.symm to e.symm_to_equiv;
• add continuous_multilinear_map.to_multilinear_map_add, continuous_multilinear_map.to_multilinear_map_smul, and simps for continuous_multilinear_map.to_multilinear_map_linear.