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
i : ι
j : κ
⊢ ↑(tensorProduct b c) (i, j) = ↑b i ⊗ₜ[R] ↑c j
simp [Basis.tensorProduct]