coe_cons_eq_coe_append — Mathlib

English

The cycle built from a list by prepending an element is the same as the cycle built from the list with that element appended to the end.

Русский

Цикл, построенный из списка путём добавления элемента спереди, равен циклу, полученному из списка, к которому этот элемент добавлен в конец.

LaTeX

$$$\text{Cycle.ofList}(a::l) = \text{Cycle.ofList}(l++[a])$$$

Lean4

theorem coe_cons_eq_coe_append (l : List α) (a : α) : (↑(a :: l) : Cycle α) = (↑(l ++ [a]) : Cycle α) :=
  Quot.sound ⟨1, by rw [rotate_cons_succ, rotate_zero]⟩

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