Theorems · Theorem · group theory

Finsupp.single_add

∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (b₁ b₂ : M),
  (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

23 results in Mathlib

Foundations

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

Assumes

AddZeroClass