Theorems · Theorem · general algebraic systems

DFinsupp.prod_eq_zero_iff

∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [inst_5 : (i : ι) → DecidableEq (β i)]
  {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ}, f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqZeroCommMonoidWithZeroNontrivialNoZeroDivisorsDecidableEq