Commit 2023-02-18 18:40 79902bfc

View on Github →

refactor: fix LinearMap.coe_mk (#2336)

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap.lean

added theorem LinearMap.coe_addHom_mk

modified theorem LinearMap.coe_mk