Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-03 16:38 a5b7de0a

View on Github →

chore(linear_algebra): fix/add coe_fn simp lemmas (#7015)

  • move @[simp] from linear_map.comp_apply to new linear_map.coe_comp;
  • rename linear_map.comp_coe to linear_map.coe_comp, swap LHS&RHS;
  • add linear_map.coe_proj, move @[simp] from linear_map.proj_apply.

Estimated changes

added theorem linear_map.coe_comp
modified theorem linear_map.comp_apply
deleted theorem linear_map.comp_coe
added theorem linear_map.coe_proj
modified theorem linear_map.proj_apply