Documentation
Mathlib
.
Data
.
Fintype
.
Vector
Search
Google site search
Mathlib
.
Data
.
Fintype
.
Vector
source
Imports
Init
Mathlib.Data.Fintype.Pi
Mathlib.Data.Sym.Basic
Imported by
Vector
.
fintype
instFintypeSym'
instFintypeSym
Vector
α n
and
Sym
α n
are fintypes when
α
is.
#
source
instance
Vector
.
fintype
{α :
Type
u_1}
[
Fintype
α
]
{n :
ℕ
}
:
Fintype
(
Vector
α
n
)
source
instance
instFintypeSym'
{α :
Type
u_1}
[
DecidableEq
α
]
[
Fintype
α
]
{n :
ℕ
}
:
Fintype
(
Sym.Sym'
α
n
)
source
instance
instFintypeSym
{α :
Type
u_1}
[
DecidableEq
α
]
[
Fintype
α
]
{n :
ℕ
}
:
Fintype
(
Sym
α
n
)