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