no goals
α : Type u_3
ι : Type ?u.341371
γ : Type ?u.341374
A : Type ?u.341377
B : Type ?u.341380
C : Type ?u.341383
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.344513
M : Type u_1
M' : Type ?u.344519
N : Type u_2
P : Type ?u.344525
G : Type ?u.344528
H : Type ?u.344531
R : Type ?u.344534
S : Type ?u.344537
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ prod (f + g) h = prod f h * prod g h
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a
no goals
α : Type u_3
ι : Type ?u.341371
γ : Type ?u.341374
A : Type ?u.341377
B : Type ?u.341380
C : Type ?u.341383
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.344513
M : Type u_1
M' : Type ?u.344519
N : Type u_2
P : Type ?u.344525
G : Type ?u.344528
H : Type ?u.344531
R : Type ?u.344534
S : Type ?u.344537
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ prod (f + g) h = prod f h * prod g h
exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a