coe_eq_coe — Mathlib

English

Two cycles are equal if and only if their underlying lists are rotated versions of each other.

Русский

Два цикла равны тогда и только тогда, когда соответствующие им списки являются вращениями друг друга.

LaTeX

$$$(l_1 : Cycle\ α) = (l_2 : Cycle\ α) \iff l_1 \sim_r l_2$$$

Lean4

@[simp]
theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Cycle α) = (l₂ : Cycle α) ↔ l₁ ~r l₂ :=
  @Quotient.eq _ (IsRotated.setoid _) _ _

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