Finite support functions

This module is almost exactly the same as Mathlib.Data.Finsupp.Defs but uses Fintype instead of Finite to make certain equivalences computable.

def equivFunOnFinite {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] : (α →₀ M) ≃ (α → M)

Equations

• equivFunOnFinite = { toFun := DFunLike.coe, invFun := fun (f : α → M) => { support := {x : α | f x ≠ 0}, toFun := f, mem_support_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem equivFunOnFinite_symm_apply_support {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] (f : α → M) : (equivFunOnFinite.symm f).support = {x : α | f x ≠ 0}

@[simp]

theorem equivFunOnFinite_apply {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] (a✝ : α →₀ M) (a : α) : equivFunOnFinite a✝ a = a✝ a

@[simp]

theorem equivFunOnFinite_symm_apply_apply {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] (f : α → M) (a✝ : α) : (equivFunOnFinite.symm f) a✝ = f a✝

@[simp]

theorem equivFunOnFinite_symm_coe {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] (f : α →₀ M) : equivFunOnFinite.symm ⇑f = f

@[simp]

theorem coe_equivFunOnFinite_symm {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] (f : α → M) : ⇑(equivFunOnFinite.symm f) = f

@[simp]

theorem equivFunOnFinite_single {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] [DecidableEq α] (x : α) (m : M) : equivFunOnFinite (Finsupp.single x m) = Pi.single x m

@[simp]

theorem equivFunOnFinite_symm_single {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq M] [Zero M] [DecidableEq α] (x : α) (m : M) : equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m