α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ (∏ᶠ (x : α), f x) = 0
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
⊢ (∏ᶠ (x : α), f x) = 0
nontriviality
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ ∏ i in Finite.toFinset hf, f i = 0
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ (∏ᶠ (x : α), f x) = 0
rw [finprod_eq_prod f hf]
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ x ∈ mulSupport f
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ ∏ i in Finite.toFinset hf, f i = 0
refine' Finset.prod_eq_zero (hf.mem_toFinset.2 _) hx
no goals
α : Type u_2
β : Type ?u.383113
ι : Type ?u.383116
G : Type ?u.383119
M : Type ?u.383122
N : Type ?u.383125
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
f : α → M₀
x : α
hx : f x = 0
hf : Set.Finite (mulSupport f)
✝ : Nontrivial M₀
⊢ x ∈ mulSupport f
simp [hx]