ι : Type u_4
ι' : Type ?u.502339
R : Type u_3
R₂ : Type ?u.502345
K : Type ?u.502348
M : Type u_2
M' : Type u_1
M'' : Type ?u.502357
V : Type u
V' : Type ?u.502362
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
S : Type u_5
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ (Finsupp.sum (Finsupp.mapDomain f (↑↑b.repr x)) fun i a => a • id i) = Finsupp.sum (↑b.repr x) fun b a => a • f b
ι : Type u_4
ι' : Type ?u.502339
R : Type u_3
R₂ : Type ?u.502345
K : Type ?u.502348
M : Type u_2
M' : Type u_1
M'' : Type ?u.502357
V : Type u
V' : Type ?u.502362
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
S : Type u_5
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ↑(↑(constr b S) f) x = Finsupp.sum (↑b.repr x) fun b a => a • f b
simp only [constr_def, LinearMap.comp_apply, Finsupp.lmapDomain_apply, Finsupp.total_apply]
no goals
ι : Type u_4
ι' : Type ?u.502339
R : Type u_3
R₂ : Type ?u.502345
K : Type ?u.502348
M : Type u_2
M' : Type u_1
M'' : Type ?u.502357
V : Type u
V' : Type ?u.502362
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
S : Type u_5
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x : M
⊢ (Finsupp.sum (Finsupp.mapDomain f (↑↑b.repr x)) fun i a => a • id i) = Finsupp.sum (↑b.repr x) fun b a => a • f b
rw [Finsupp.sum_mapDomain_index] <;> simp [add_smul]