Commit 2021-02-13 07:17 ee9197a1

chore(topology/algebra/module): review coe lemmas (#6206)

• add @[simp] to continuous_linear_equiv.coe_coe, remove from continuous_linear_equiv.coe_apply;
• golf continuous_linear_equiv.ext;
• given (e e' : M ≃L[R] M₂), simplify (e : M →L[R] M₂) = e' to e = e';
• add @[simp] to continuous_linear_equiv.symm_comp_self and continuous_linear_equiv.self_comp_symm;
• drop symm_comp_self' and self_comp_symm': now coe_coe simplifies LHS to symm_comp_self/self_comp_symm;
• continuous_linear_equiv.coord is no longer an abbreviation: without this change coe_coe prevents us from using lemmas about coord;