Theorems · Theorem · general algebraic systems

Finsupp.zipWith_single_single

∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
  (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N),
  (Finsupp.zipWith f hf (fun₀ | a => m) fun₀ | a => n) = fun₀ | a => f m n

Defined in

Mathlib.Data.Finsupp.Single

Cited by

2 results in Mathlib

Foundations

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

Assumes

ZeroZeroZero