Mathlib.Logic.Equiv.Fin.Rotate

finRotate definition

: ∀ n, Equiv.Perm (Fin n)

Full source

/-- Rotate `Fin n` one step to the right. -/
def finRotate : ∀ n, Equiv.Perm (Fin n)
  | 0 => Equiv.refl _
  | n + 1 => finAddFlip.trans (finCongr (Nat.add_comm 1 n))

Right cyclic permutation on $\mathrm{Fin}(n)$

Informal description

For each natural number $ n $, the function $\mathrm{finRotate}(n)$ defines a cyclic permutation on the finite type $\mathrm{Fin}(n)$ that rotates the elements one step to the right. Specifically: - When $ n = 0 $, it is the identity permutation on $\mathrm{Fin}(0)$. - For $ n + 1 $, it is the composition of the flip permutation $\mathrm{finAddFlip}$ and the equivalence $\mathrm{finCongr}$ induced by the equality $1 + n = n + 1$.

finRotate_zero theorem

: finRotate 0 = Equiv.refl _

Full source

@[simp] lemma finRotate_zero : finRotate 0 = Equiv.refl _ := rfl

Identity Property of `finRotate` at Zero

Informal description

The cyclic permutation `finRotate` on the finite type $\mathrm{Fin}(0)$ is equal to the identity permutation.

finRotate_succ theorem

(n : ℕ) : finRotate (n + 1) = finAddFlip.trans (finCongr (Nat.add_comm 1 n))

Full source

lemma finRotate_succ (n : ℕ) :
    finRotate (n + 1) = finAddFlip.trans (finCongr (Nat.add_comm 1 n)) := rfl

Recursive Construction of Cyclic Permutation on $\mathrm{Fin}(n+1)$ via Addition Commutativity

Informal description

For any natural number $n$, the cyclic permutation $\mathrm{finRotate}(n+1)$ on $\mathrm{Fin}(n+1)$ is equal to the composition of the flip permutation $\mathrm{finAddFlip}$ with the equivalence $\mathrm{finCongr}$ induced by the commutativity of addition $1 + n = n + 1$.

finRotate_of_lt theorem

{k : ℕ} (h : k < n) : finRotate (n + 1) ⟨k, h.trans_le n.le_succ⟩ = ⟨k + 1, Nat.succ_lt_succ h⟩

Full source

theorem finRotate_of_lt {k : ℕ} (h : k < n) :
    finRotate (n + 1) ⟨k, h.trans_le n.le_succ⟩ = ⟨k + 1, Nat.succ_lt_succ h⟩ := by
  ext
  dsimp [finRotate_succ]
  simp [finAddFlip_apply_mk_left h, Nat.add_comm]

Right Cyclic Permutation Maps Element $k$ to $k+1$ in $\mathrm{Fin}(n+1)$ When $k < n$

Informal description

For any natural numbers $k$ and $n$ such that $k < n$, the right cyclic permutation $\mathrm{finRotate}(n+1)$ maps the element $\langle k, h \rangle$ of $\mathrm{Fin}(n+1)$ (where $h$ is a proof that $k < n$) to the element $\langle k+1, h' \rangle$, where $h'$ is a proof that $k+1 < n+1$.

finRotate_last' theorem

: finRotate (n + 1) ⟨n, by omega⟩ = ⟨0, Nat.zero_lt_succ _⟩

Full source

theorem finRotate_last' : finRotate (n + 1) ⟨n, by omega⟩ = ⟨0, Nat.zero_lt_succ _⟩ := by
  dsimp [finRotate_succ]
  rw [finAddFlip_apply_mk_right le_rfl]
  simp

Right Cyclic Permutation Maps Last Element to Zero in $\mathrm{Fin}(n+1)$

Informal description

For any natural number $ n $, the right cyclic permutation $\mathrm{finRotate}(n+1)$ maps the element $\langle n, h \rangle$ of $\mathrm{Fin}(n+1)$ (where $ h $ is a proof that $ n < n+1 $) to the element $\langle 0, \mathrm{Nat.zero\_lt\_succ}\, n \rangle$, which is the zero element of $\mathrm{Fin}(n+1)$.

finRotate_last theorem

: finRotate (n + 1) (Fin.last _) = 0

Full source

theorem finRotate_last : finRotate (n + 1) (Fin.last _) = 0 :=
  finRotate_last'

Right Cyclic Permutation Maps Last Element to Zero in $\mathrm{Fin}(n+1)$

Informal description

For any natural number $n$, the right cyclic permutation $\mathrm{finRotate}(n+1)$ maps the last element $\mathrm{Fin.last}(n)$ of $\mathrm{Fin}(n+1)$ to the zero element $0$ of $\mathrm{Fin}(n+1)$.

Fin.snoc_eq_cons_rotate theorem

 {α : Type*} (v : Fin n → α) (a : α) :
  @Fin.snoc _ (fun _ => α) v a = fun i => @Fin.cons _ (fun _ => α) a v (finRotate _ i)

Full source

theorem Fin.snoc_eq_cons_rotate {α : Type*} (v : Fin n → α) (a : α) :
    @Fin.snoc _ (fun _ => α) v a = fun i => @Fin.cons _ (fun _ => α) a v (finRotate _ i) := by
  ext ⟨i, h⟩
  by_cases h' : i < n
  · rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
    rfl
  · have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
    subst h''
    rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
    rfl

Equivalence of Snoc and Cons with Cyclic Permutation on Finite Types

Informal description

For any type $\alpha$, a function $v : \mathrm{Fin}(n) \to \alpha$, and an element $a : \alpha$, the function $\mathrm{snoc}(v, a)$ obtained by appending $a$ to $v$ is equal to the function $\mathrm{cons}(a, v)$ composed with the cyclic permutation $\mathrm{finRotate}$ on $\mathrm{Fin}(n+1)$. In other words, for any $i \in \mathrm{Fin}(n+1)$, we have $\mathrm{snoc}(v, a)(i) = \mathrm{cons}(a, v)(\mathrm{finRotate}(i))$.

finRotate_one theorem

: finRotate 1 = Equiv.refl _

Full source

@[simp]
theorem finRotate_one : finRotate 1 = Equiv.refl _ :=
  Subsingleton.elim _ _

Identity Property of `finRotate` on $\mathrm{Fin}(1)$

Informal description

The cyclic permutation `finRotate` on the finite type $\mathrm{Fin}(1)$ is equal to the identity permutation.

finRotate_succ_apply theorem

(i : Fin (n + 1)) : finRotate (n + 1) i = i + 1

Full source

@[simp] theorem finRotate_succ_apply (i : Fin (n + 1)) : finRotate (n + 1) i = i + 1 := by
  cases n
  · exact @Subsingleton.elim (Fin 1) _ _ _
  obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
  · simp [finRotate_last]
  · cases i
    simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_mk] at h
    simp [finRotate_of_lt h, Fin.ext_iff, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

Right Cyclic Permutation Maps $i$ to $i+1$ in $\mathrm{Fin}(n+1)$

Informal description

For any element $i$ in the finite type $\mathrm{Fin}(n+1)$, the right cyclic permutation $\mathrm{finRotate}(n+1)$ maps $i$ to $i + 1$.

finRotate_apply_zero theorem

: finRotate n.succ 0 = 1

Full source

theorem finRotate_apply_zero : finRotate n.succ 0 = 1 := by
  simp

Zero maps to one under right cyclic permutation on $\mathrm{Fin}(n+1)$

Informal description

For any natural number $n$, the right cyclic permutation $\mathrm{finRotate}(n+1)$ maps the zero element $0 \in \mathrm{Fin}(n+1)$ to the element $1 \in \mathrm{Fin}(n+1)$.

coe_finRotate_of_ne_last theorem

{i : Fin n.succ} (h : i ≠ Fin.last n) : (finRotate (n + 1) i : ℕ) = i + 1

Full source

theorem coe_finRotate_of_ne_last {i : Fin n.succ} (h : i ≠ Fin.last n) :
    (finRotate (n + 1) i : ℕ) = i + 1 := by
  rw [finRotate_succ_apply]
  have : (i : ℕ) < n := Fin.val_lt_last h
  exact Fin.val_add_one_of_lt this

Natural Number Representation of Non-Last Element Under Cyclic Permutation

Informal description

For any element $i$ in $\mathrm{Fin}(n+1)$ that is not the last element (i.e., $i \neq \mathrm{last}(n)$), the natural number corresponding to the image of $i$ under the right cyclic permutation $\mathrm{finRotate}(n+1)$ is $i + 1$. In other words, if $i \neq \mathrm{last}(n)$, then $(\mathrm{finRotate}(n+1)(i) : \mathbb{N}) = i + 1$.

coe_finRotate theorem

(i : Fin n.succ) : (finRotate n.succ i : ℕ) = if i = Fin.last n then (0 : ℕ) else i + 1

Full source

theorem coe_finRotate (i : Fin n.succ) :
    (finRotate n.succ i : ℕ) = if i = Fin.last n then (0 : ℕ) else i + 1 := by
  rw [finRotate_succ_apply, Fin.val_add_one i]

Natural Number Representation of Right Cyclic Permutation on $\mathrm{Fin}(n+1)$

Informal description

For any element $i$ in $\mathrm{Fin}(n+1)$, the natural number corresponding to $\mathrm{finRotate}(n+1)(i)$ is $0$ if $i$ is the last element of $\mathrm{Fin}(n+1)$, and $i + 1$ otherwise. In other words: \[ \mathrm{finRotate}(n+1)(i) = \begin{cases} 0 & \text{if } i = \mathrm{last}(n), \\ i + 1 & \text{otherwise.} \end{cases} \]

lt_finRotate_iff_ne_last theorem

(i : Fin (n + 1)) : i < finRotate _ i ↔ i ≠ Fin.last n

Full source

theorem lt_finRotate_iff_ne_last (i : Fin (n + 1)) :
    i < finRotate _ i ↔ i ≠ Fin.last n := by
  refine ⟨fun hi hc ↦ ?_, fun hi ↦ ?_⟩
  · simp only [hc, finRotate_succ_apply, Fin.last_add_one, Fin.not_lt_zero] at hi
  · rw [Fin.lt_iff_val_lt_val, coe_finRotate_of_ne_last hi, Nat.lt_add_one_iff]

Inequality Under Cyclic Permutation Characterizes Non-Last Element in $\mathrm{Fin}(n+1)$

Informal description

For any element $i$ in $\mathrm{Fin}(n+1)$, the inequality $i < \mathrm{finRotate}(n+1)(i)$ holds if and only if $i$ is not the last element of $\mathrm{Fin}(n+1)$ (i.e., $i \neq \mathrm{last}(n)$).

lt_finRotate_iff_ne_neg_one theorem

[NeZero n] (i : Fin n) : i < finRotate _ i ↔ i ≠ -1

Full source

theorem lt_finRotate_iff_ne_neg_one [NeZero n] (i : Fin n) :
    i < finRotate _ i ↔ i ≠ -1 := by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ←Fin.neg_last, neg_neg]

Inequality Under Cyclic Permutation Characterizes Non-Negative-One Element in $\mathrm{Fin}(n)$

Informal description

For any nonzero natural number $ n $ and any element $ i $ in the finite type $\mathrm{Fin}(n)$, the inequality $ i < \mathrm{finRotate}(n)(i) $ holds if and only if $ i $ is not equal to $-1$ (i.e., the last element of $\mathrm{Fin}(n)$ under negation).

finRotate_succ_symm_apply theorem

[NeZero n] (i : Fin n) : (finRotate _).symm i = i - 1

Full source

@[simp] lemma finRotate_succ_symm_apply [NeZero n] (i : Fin n) : (finRotate _).symm i = i - 1 := by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  apply (finRotate n.succ).symm_apply_eq.mpr
  rw [finRotate_succ_apply, sub_add_cancel]

Inverse of Right Cyclic Permutation Maps $ i $ to $ i - 1 $ in $\mathrm{Fin}(n)$

Informal description

For any nonzero natural number $ n $ and any element $ i $ in the finite type $\mathrm{Fin}(n)$, the inverse of the right cyclic permutation $\mathrm{finRotate}(n)$ maps $ i $ to $ i - 1 $.

coe_finRotate_symm_of_ne_zero theorem

[NeZero n] {i : Fin n} (hi : i ≠ 0) : ((finRotate _).symm i : ℕ) = i - 1

Full source

lemma coe_finRotate_symm_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) :
    ((finRotate _).symm i : ℕ) = i - 1 := by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rwa [finRotate_succ_symm_apply, Fin.val_sub_one_of_ne_zero]

Natural Number Value of Inverse Cyclic Permutation: $(\mathrm{finRotate}(n)^{-1}(i))_\mathbb{N} = i - 1$ for $i \neq 0$

Informal description

For any nonzero natural number $ n $ and any nonzero element $ i $ in the finite type $\mathrm{Fin}(n)$, the underlying natural number value of the inverse of the right cyclic permutation $\mathrm{finRotate}(n)$ applied to $ i $ is equal to $ i - 1 $. That is, $(\mathrm{finRotate}(n)^{-1}(i))_\mathbb{N} = i - 1$ when $ i \neq 0 $.

finRotate_symm_lt_iff_ne_zero theorem

[NeZero n] (i : Fin n) : (finRotate _).symm i < i ↔ i ≠ 0

Full source

theorem finRotate_symm_lt_iff_ne_zero [NeZero n] (i : Fin n) :
    (finRotate _).symm i < i ↔ i ≠ 0 := by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  refine ⟨fun hi hc ↦ ?_, fun hi ↦ ?_⟩
  · simp only [hc, Fin.last_add_one, Fin.not_lt_zero] at hi
  · rw [Fin.lt_iff_val_lt_val, coe_finRotate_symm_of_ne_zero hi]
    apply sub_lt (zero_lt_of_ne_zero <| Fin.val_ne_zero_iff.mpr hi) Nat.zero_lt_one

Inverse Cyclic Permutation Strictly Decreases Nonzero Elements in $\mathrm{Fin}(n)$

Informal description

For any nonzero natural number $n$ and any element $i$ in $\mathrm{Fin}(n)$, the inverse of the right cyclic permutation $\mathrm{finRotate}(n)$ maps $i$ to an element strictly less than $i$ if and only if $i$ is not equal to zero. That is, $\mathrm{finRotate}(n)^{-1}(i) < i \leftrightarrow i \neq 0$.