Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.map_op_smul'

Modification history

2022-03-16 19:40
src/data/matrix/basic.lean
feat(algebra/algebra/basic,data/matrix/basic): resolve a TODO about `alg_hom.map_smul_of_tower` (#12684) …
Added matrix.map_op_smul'View on Github →