Documentation
Batteries
.
Data
.
Fin
.
Lemmas
Search
Google site search
return to top
source
Imports
Init
Batteries.Data.Fin.Basic
Batteries.Data.List.Lemmas
Imported by
Fin
.
coe_clamp
clamp
#
source
@[simp]
theorem
Fin
.
coe_clamp
(n m :
Nat
)
:
↑
(
Fin.clamp
n
m
)
=
min
n
m