HepLean Documentation
Init
.
Data
.
Fin
.
Log2
Search
Google site search
return to top
source
Imports
Init.Data.Nat.Log2
Imported by
Fin
.
log2
source
def
Fin
.
log2
{m :
Nat
}
(n :
Fin
m
)
:
Fin
m
Equations
n
.log2
=
⟨
(↑
n
)
.log2
,
⋯
⟩
Instances For