mathlib3

bfd06851 - fix(algebra/module/linear_map): do not introduce `show` (#8102)

fix(algebra/module/linear_map): do not introduce `show` (#8102) Without this change, `apply linear_map.coe_injective` on a goal of `f = g` introduces some unpleasant `show` terms, giving a goal of ```lean (λ (f : M →ₗ[R] M₂), show M → M₂, from ⇑f) f = (λ (f : M →ₗ[R] M₂), show M → M₂, from ⇑f) g ``` which is then frustrating to `rw` at, instead of ```lean ⇑f = ⇑g ```