no goals
R : Type u_1
R₁ : Type ?u.1372557
R₂ : Type ?u.1372560
M : Type ?u.1372563
M₁ : Type u_2
M₂ : Type u_3
M₁' : Type ?u.1372572
M₂' : Type ?u.1372575
n : Type u_4
m : Type u_5
n' : Type ?u.1372584
m' : Type ?u.1372587
ι : Type ?u.1372590
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 : M₁ →ₗ[R] M₂ →ₗ[R] R
i : n
j : m
⊢ ↑(toMatrix₂Aux ↑b₁ ↑b₂) B i j = ↑(toMatrix₂ b₁ b₂) B i j
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]