α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
⊢ (∏ᶠ (ab : α × β), f ab) = ∏ᶠ (a : α) (b : β), f (a, b)
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
⊢ (∏ᶠ (ab : α × β), f ab) = ∏ᶠ (a : α) (b : β), f (a, b)
have h₁ : ∀ a, (∏ᶠ _ : a ∈ hf.toFinset, f a) = f a := by simp
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
h₂ : (∏ᶠ (a : α × β), f a) = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ (∏ᶠ (ab : α × β), f ab) = ∏ᶠ (a : α) (b : β), f (a, b)
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
⊢ (∏ᶠ (ab : α × β), f ab) = ∏ᶠ (a : α) (b : β), f (a, b)
have h₂ : (∏ᶠ a, f a) = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
h₂ : (∏ᶠ (a : α × β), f a) = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ (∏ᶠ (ab : α × β), f ab) = ∏ᶠ (a : α) (b : β), f (a, b)
simp_rw [h₂, finprod_mem_finset_product, h₁]
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
⊢ ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
simp
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.456339
G : Type ?u.456342
M : Type u_3
N : Type ?u.456348
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α × β → M
hf : Set.Finite (mulSupport f)
h₁ : ∀ (a : α × β), (∏ᶠ (_ : a ∈ Finite.toFinset hf), f a) = f a
⊢ (∏ᶠ (a : α × β), f a) = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
simp