Mathlib Map

Theorems · Definition · general algebraic systems

DFinsupp.toFun

{ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → DFinsupp β → (i : ι) → β i

The underlying function of a dependent function with finite support (aka DFinsupp).

Defined in
Mathlib.Data.DFinsupp.Defs
Cited by
5 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Zero
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DFinsupp.support · cited by 158DFinsupp.supportDFinsupp.erase · cited by 29DFinsupp.eraseDFinsupp.mapRange · cited by 29DFinsupp.mapRangeDFinsupp.filter · cited by 24DFinsupp.filterDFinsupp.subtypeDomain · cited by 14DFinsupp.subtypeDomainMultilinearMap.dfinsuppFamily · cited by 13MultilinearMap.dfinsuppFa…DFinsupp.comapDomain' · cited by 9DFinsupp.comapDomain'DFinsupp.update · cited by 8DFinsupp.updateDFinsupp.comapDomain · cited by 8DFinsupp.comapDomainDFinsupp.zipWith · cited by 7DFinsupp.zipWithDFinsupp.sigmaCurry · cited by 6DFinsupp.sigmaCurryDFinsupp.sumZeroHom · cited by 6DFinsupp.sumZeroHomDFinsupp.extendWith · cited by 5DFinsupp.extendWithDFinsupp.support' · cited by 5DFinsupp.support'DFinsupp.rangeIcc · cited by 5DFinsupp.rangeIccDFinsupp · cited by 694DFinsuppDFinsupp.toFunCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFinsuppstatement and proof · cited by 694

Cited by22

Results whose statement or proof uses this declaration.