Documentation
SpherePacking
.
ForMathlib
.
Vec
Search
return to top
source
Imports
Init
Mathlib.Data.Fin.VecNotation
Imported by
Matrix
.
cons_val_five
Matrix
.
cons_val_six
Matrix
.
cons_val_seven
source
@[simp]
theorem
Matrix
.
cons_val_five
{
m
:
ℕ
}
{
α
:
Type
u_1}
(
x
:
α
)
(
u
:
Fin
m
.
succ
.
succ
.
succ
.
succ
.
succ
→
α
)
:
vecCons
x
u
5
=
vecHead
(
vecTail
(
vecTail
(
vecTail
(
vecTail
u
)
)
)
)
source
@[simp]
theorem
Matrix
.
cons_val_six
{
m
:
ℕ
}
{
α
:
Type
u_1}
(
x
:
α
)
(
u
:
Fin
m
.
succ
.
succ
.
succ
.
succ
.
succ
.
succ
→
α
)
:
vecCons
x
u
6
=
vecHead
(
vecTail
(
vecTail
(
vecTail
(
vecTail
(
vecTail
u
)
)
)
)
)
source
@[simp]
theorem
Matrix
.
cons_val_seven
{
m
:
ℕ
}
{
α
:
Type
u_1}
(
x
:
α
)
(
u
:
Fin
m
.
succ
.
succ
.
succ
.
succ
.
succ
.
succ
.
succ
→
α
)
:
vecCons
x
u
7
=
vecHead
(
vecTail
(
vecTail
(
vecTail
(
vecTail
(
vecTail
(
vecTail
u
)
)
)
)
)
)