α : Type u_3
ι : Type ?u.531151
γ : Type ?u.531154
A : Type ?u.531157
B : Type ?u.531160
C : Type ?u.531163
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_4
M : Type u_1
M' : Type ?u.534299
N : Type u_2
P : Type ?u.534305
G : Type ?u.534308
H : Type ?u.534311
R : Type ?u.534314
S : Type ?u.534317
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x in v.support, g (↑f x) (↑(embDomain f v) (↑f x)) = ∏ a in v.support, g (↑f a) (↑v a)
α : Type u_3
ι : Type ?u.531151
γ : Type ?u.531154
A : Type ?u.531157
B : Type ?u.531160
C : Type ?u.531163
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_4
M : Type u_1
M' : Type ?u.534299
N : Type u_2
P : Type ?u.534305
G : Type ?u.534308
H : Type ?u.534311
R : Type ?u.534314
S : Type ?u.534317
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ prod (embDomain f v) g = prod v fun a b => g (↑f a) b
rw [prod, prod, support_embDomain, Finset.prod_map]
no goals
α : Type u_3
ι : Type ?u.531151
γ : Type ?u.531154
A : Type ?u.531157
B : Type ?u.531160
C : Type ?u.531163
inst✝⁴ : AddCommMonoid A
inst✝³ : AddCommMonoid B
inst✝² : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_4
M : Type u_1
M' : Type ?u.534299
N : Type u_2
P : Type ?u.534305
G : Type ?u.534308
H : Type ?u.534311
R : Type ?u.534314
S : Type ?u.534317
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x in v.support, g (↑f x) (↑(embDomain f v) (↑f x)) = ∏ a in v.support, g (↑f a) (↑v a)
simp_rw [embDomain_apply]