Theorems · Inductive type · general algebraic systems

DFinsupp

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

A dependent function Π i, β i with finite support, with notation Π₀ i, β i. Note that DFinsupp.support is the preferred API for accessing the support of the function, DFinsupp.support' is an implementation detail that aids computability; see the implementation notes in this file for more information.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

694 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Zero