Documentation
FormalConjectures
.
ForMathlib
.
Logic
.
Equiv
.
Fin
.
Rotate
Search
return to top
source
Imports
Init
Mathlib.Logic.Equiv.Fin.Rotate
Imported by
lt_finRotate_of_ne_last
source
theorem
lt_finRotate_of_ne_last
{
n
:
ℕ
}
{
i
:
Fin
(
n
+
1
)
}
(
hi
:
i
≠
Fin.last
n
)
:
i
<
(
finRotate
(
n
+
1
))
i