no goals
R : Type u_2
M : Type u_3
N : Type u_5
ι : Type u_1
κ : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
m : M
n : N
i : ι
j : κ
⊢ ↑(↑(tensorProduct b c).repr (m ⊗ₜ[R] n)) (i, j) = ↑(↑b.repr m) i * ↑(↑c.repr n) j
simp [Basis.tensorProduct]