cycleRange_last — Mathlib

English

Let n be a natural number. The cycleRange associated to the last element of Fin n coincides with the standard cyclic permutation finRotate of size n+1.

Русский

Пусть n — натуральное число. Циклическое Range, связанное с последним элементом Fin n, совпадает с обычной циклической перестановкой размера n+1.

LaTeX

$$$\operatorname{cycleRange}(\mathrm{last}\, n) = \operatorname{finRotate}(n+1)$$$

Lean4

@[simp]
theorem cycleRange_last (n : ℕ) : cycleRange (last n) = finRotate (n + 1) :=
  by
  ext i
  rw [coe_cycleRange_of_le (le_last _), coe_finRotate]

Похожие утверждения