HepLean Documentation
Mathlib
.
Data
.
Finite
.
Vector
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Card
Mathlib.Data.Fintype.Vector
Imported by
Mathlib
.
Vector
.
finite
Finiteness of vector types
#
source
instance
Mathlib
.
Vector
.
finite
{α :
Type
u_1}
[
Finite
α
]
{n :
ℕ
}
:
Finite
(
Mathlib.Vector
α
n
)
Equations
⋯
=
⋯