Theorems · Theorem · general algebraic systems

Finsupp.support_zipWith

∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  [D : DecidableEq α] {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N},
  (Finsupp.zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

ZeroZeroZeroDecidableEq