ι : Type ?u.875346
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ (¬∃ a, a ∈ s ∧ f a = 0) ↔ ∀ (a : α), a ∈ s → f a ≠ 0
ι : Type ?u.875346
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ ∏ x in s, f x ≠ 0 ↔ ∀ (a : α), a ∈ s → f a ≠ 0
rw [Ne, prod_eq_zero_iff]
ι : Type ?u.875346
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ (∀ (a : α), a ∈ s → f a ≠ 0) ↔ ∀ (a : α), a ∈ s → f a ≠ 0
ι : Type ?u.875346
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ (¬∃ a, a ∈ s ∧ f a = 0) ↔ ∀ (a : α), a ∈ s → f a ≠ 0
push_neg
no goals
ι : Type ?u.875346
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoidWithZero β
inst✝¹ : Nontrivial β
inst✝ : NoZeroDivisors β
⊢ (∀ (a : α), a ∈ s → f a ≠ 0) ↔ ∀ (a : α), a ∈ s → f a ≠ 0
rfl