no goals
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.1190163
l : Type ?u.1190166
m : Type ?u.1190169
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] n → R
i j : n
⊢ ↑toMatrixAlgEquiv' f i j = ↑f (fun j' => if j' = j then 1 else 0) i
simp [LinearMap.toMatrixAlgEquiv']