case h.a.h
R : Type u_1
R₁ : Type ?u.1414675
R₂ : Type ?u.1414678
M : Type ?u.1414681
M₁ : Type ?u.1414684
M₂ : Type ?u.1414687
M₁' : Type ?u.1414690
M₂' : Type ?u.1414693
n : Type u_2
m : Type u_3
n' : Type ?u.1414702
m' : Type ?u.1414705
ι : Type ?u.1414708
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
i✝ : n
x✝ : m
⊢ ↑(toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ x✝ = ↑toMatrix₂' B i✝ x✝
R : Type u_1
R₁ : Type ?u.1414675
R₂ : Type ?u.1414678
M : Type ?u.1414681
M₁ : Type ?u.1414684
M₂ : Type ?u.1414687
M₁' : Type ?u.1414690
M₂' : Type ?u.1414693
n : Type u_2
m : Type u_3
n' : Type ?u.1414702
m' : Type ?u.1414705
ι : Type ?u.1414708
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
⊢ toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = toMatrix₂'
ext B
no goals
case h.a.h
R : Type u_1
R₁ : Type ?u.1414675
R₂ : Type ?u.1414678
M : Type ?u.1414681
M₁ : Type ?u.1414684
M₂ : Type ?u.1414687
M₁' : Type ?u.1414690
M₂' : Type ?u.1414693
n : Type u_2
m : Type u_3
n' : Type ?u.1414702
m' : Type ?u.1414705
ι : Type ?u.1414708
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
i✝ : n
x✝ : m
⊢ ↑(toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m)) B i✝ x✝ = ↑toMatrix₂' B i✝ x✝
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]