Theorems · Theorem · general algebraic systems

Finsupp.sumElim_single_single

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddMonoid M] (a : α) (b : β) (m₁ m₂ : M),
  ((fun₀ | a => m₁).sumElim fun₀ | b => m₂) = (fun₀ | Sum.inl a => m₁) + fun₀ | Sum.inr b => m₂

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoid