α : Type u_3
M : Type u_4
N : Type ?u.454082
P : Type ?u.454085
R : Type u_2
S : Type ?u.454091
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_1
M' : Type ?u.454186
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ (sum (comapDomain f l hf) fun i a => a • v i) = ∑ i in Finset.preimage l.support f hf, ↑l (f i) • v i
α : Type u_3
M : Type u_4
N : Type ?u.454082
P : Type ?u.454085
R : Type u_2
S : Type ?u.454091
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_1
M' : Type ?u.454186
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ↑(Finsupp.total α M R v) (comapDomain f l hf) = ∑ i in Finset.preimage l.support f hf, ↑l (f i) • v i
rw [Finsupp.total_apply]
no goals
α : Type u_3
M : Type u_4
N : Type ?u.454082
P : Type ?u.454085
R : Type u_2
S : Type ?u.454091
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type u_1
M' : Type ?u.454186
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v : α → M
v' : α' → M'
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ (sum (comapDomain f l hf) fun i a => a • v i) = ∑ i in Finset.preimage l.support f hf, ↑l (f i) • v i
rfl