Documentation
FormalConjectures
.
ForMathlib
.
Logic
.
Equiv
.
Fin
Search
return to top
source
Imports
Init
Mathlib.Logic.Equiv.Fin
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