Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 07:17 ee9197a1

View on Github →

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;

Estimated changes