Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-24 13:18 2ed48468

View on Github →

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

Estimated changes

Modified src/linear_algebra/multilinear.lean

added theorem multilinear_map.coe_inj

added theorem multilinear_map.coe_mk

added theorem multilinear_map.congr_arg

added theorem multilinear_map.congr_fun

added theorem multilinear_map.ext_iff

added theorem multilinear_map.to_fun_eq_coe