length_mem_cyclicPermutations — Mathlib

English

If l' is a cyclic permutation of l, then their lengths are equal.

Русский

Если l' является циклической перестановкой l, то их длины равны.

LaTeX

$$$$\forall l,l' : \mathrm{List}(\alpha),\ l' \in \operatorname{cyclicPermutations}(l) \Rightarrow \operatorname{length}(l') = \operatorname{length}(l).$$$$

Lean4

theorem length_mem_cyclicPermutations (l : List α) (h : l' ∈ cyclicPermutations l) : length l' = length l :=
  by
  obtain ⟨k, hk, rfl⟩ := get_of_mem h
  simp

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