Theorems · Theorem · general algebraic systems

Finsupp.restrictSupportEquiv_symm_apply_coe

∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M] [inst_1 : DecidablePred fun x => x ∈ s]
  (f : ↑s →₀ M), ↑((Finsupp.restrictSupportEquiv s M).symm f) = f.extendDomain

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidablePred