Theorems · Theorem · general algebraic systems

Finsupp.single_eq_single_iff

∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a₁ a₂ : α) (b₁ b₂ : M),
  ((fun₀ | a₁ => b₁) = fun₀ | a₂ => b₂) ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Defined in

Mathlib.Data.Finsupp.Single

Cited by

6 results in Mathlib

Foundations

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

Assumes

Zero