ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', ↑(↑b.repr (↑b' j)) i * ↑(↑b'.repr x) j = ↑(↑b.repr (∑ i : ι', ↑(↑b'.repr x) i • ↑b' i)) i
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', ↑(↑b.repr (↑b' j)) i * ↑(↑b'.repr x) j = ↑(↑b.repr x) i
conv_rhs => rw [← b'.sum_repr x]
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ x_1 : ι', ↑(↑b.repr (↑b' x_1)) i * ↑(↑b'.repr x) x_1 = ∑ x_1 : ι', ↑(↑(↑b'.repr x) x_1 • ↑b.repr (↑b' x_1)) i
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j : ι', ↑(↑b.repr (↑b' j)) i * ↑(↑b'.repr x) j = ↑(↑b.repr (∑ i : ι', ↑(↑b'.repr x) i • ↑b' i)) i
simp_rw [LinearEquiv.map_sum, LinearEquiv.map_smul, Finset.sum_apply']
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ ↑(↑b.repr (↑b' j)) i * ↑(↑b'.repr x) j = ↑(↑(↑b'.repr x) j • ↑b.repr (↑b' j)) i
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ x_1 : ι', ↑(↑b.repr (↑b' x_1)) i * ↑(↑b'.repr x) x_1 = ∑ x_1 : ι', ↑(↑(↑b'.repr x) x_1 • ↑b.repr (↑b' x_1)) i
refine' Finset.sum_congr rfl fun j _ => _
no goals
ι : Type u_4
ι'✝ : Type ?u.761324
R : Type u_2
R₂ : Type ?u.761330
K : Type ?u.761333
M : Type u_3
M' : Type ?u.761339
M'' : Type ?u.761342
V : Type u
V' : Type ?u.761347
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b'✝ : Basis ι'✝ R M'
ι' : Type u_1
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
j : ι'
x✝ : j ∈ Finset.univ
⊢ ↑(↑b.repr (↑b' j)) i * ↑(↑b'.repr x) j = ↑(↑(↑b'.repr x) j • ↑b.repr (↑b' j)) i
rw [Finsupp.smul_apply, smul_eq_mul, mul_comm]