R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ ↑(AlgEquiv.symm (matrixEquivTensor R A n)) (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
simp [matrixEquivTensor, MatrixEquivTensor.toFunAlgHom, algHomOfLinearMapTensorProduct,
  MatrixEquivTensor.toFunLinear]
no goals
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
rfl