R : Type u_2
inst✝⁴ : CommSemiring R
k : Type ?u.752944
l : Type u_1
m : Type u_4
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ comp f g = ↑toLin' (↑toMatrix' f ⬝ ↑toMatrix' g)
R : Type u_2
inst✝⁴ : CommSemiring R
k : Type ?u.752944
l : Type u_1
m : Type u_4
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ ↑toMatrix' (comp f g) = ↑toMatrix' f ⬝ ↑toMatrix' g
suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f ⬝ LinearMap.toMatrix' g) by
  rw [this, LinearMap.toMatrix'_toLin']
no goals
R : Type u_2
inst✝⁴ : CommSemiring R
k : Type ?u.752944
l : Type u_1
m : Type u_4
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ comp f g = ↑toLin' (↑toMatrix' f ⬝ ↑toMatrix' g)
rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']
no goals
R : Type u_2
inst✝⁴ : CommSemiring R
k : Type ?u.752944
l : Type u_1
m : Type u_4
n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this : comp f g = ↑toLin' (↑toMatrix' f ⬝ ↑toMatrix' g)
⊢ ↑toMatrix' (comp f g) = ↑toMatrix' f ⬝ ↑toMatrix' g
rw [this, LinearMap.toMatrix'_toLin']