Theorems · Theorem · general algebraic systems

Finsupp.restrictSupportEquiv_symm_single

∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M] (a : ↑s) (x : M),
  ↑((Finsupp.restrictSupportEquiv s M).symm fun₀ | a => x) = fun₀ | ↑a => x

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoid