Documentation

Mathlib.Logic.Small.List

Instances for Small (List α) and Small (Vector α). #

These must not be in Logic.Small.Basic as this is very low in the import hierarchy, and is used by category theory files which do not need everything imported by Data.Vector.Basic.

source
instance smallVector {α : Type v} {n : ℕ} [Small.{u, v} α] :
Small.{u, v} (Mathlib.Vector α n)
Equations
  • ⋯ = ⋯
source
instance smallList {α : Type v} [Small.{u, v} α] :
Small.{u, v} (List α)
Equations
  • ⋯ = ⋯