mathlib3

2ed48468 - chore(linear_algebra/multilinear_map): Add boring coercion lemmas copied from ring_hom (#5099)