Commit 2021-06-28 10:36 bfd06851

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

(λ (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

⇑f = ⇑g