Documentation
Std
.
Data
.
Fin
.
Init
.
Lemmas
Search
Google site search
Std
.
Data
.
Fin
.
Init
.
Lemmas
source
Imports
Init
Imported by
Fin
.
zero_eta
source
@[simp]
theorem
Fin
.
zero_eta
{n :
Nat
}
:
{
val
:=
0
,
isLt
:=
(_ :
0
<
Nat.succ
n
)
}
=
0