[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
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
[PROOFSTEP]
simp [Basis.tensorProduct]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
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 : ι × κ
⊢ ↑(tensorProduct b c) i = ↑b i.fst ⊗ₜ[R] ↑c i.snd
[PROOFSTEP]
simp [Basis.tensorProduct]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
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
[PROOFSTEP]
simp [Basis.tensorProduct]