no goals
α : Type u_1
β : Type ?u.185720
ι : Type ?u.185723
G : Type ?u.185726
M : Type u_2
N : Type ?u.185732
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Infinite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = 1
classical rw [finprod_def, dif_neg hf]
no goals
α : Type u_1
β : Type ?u.185720
ι : Type ?u.185723
G : Type ?u.185726
M : Type u_2
N : Type ?u.185732
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
hf : Set.Infinite (mulSupport f)
⊢ (∏ᶠ (i : α), f i) = 1
rw [finprod_def, dif_neg hf]