cyclicPermutations_inj — Mathlib

English

Let l and l' be lists over a type α. If their cyclic permutations are equal, then l = l'.

Русский

Пусть l и l' — списки над некоторым типом α. Если их циклические перестановки равны, то l = l'.

LaTeX

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

Lean4

@[simp]
theorem cyclicPermutations_inj {l l' : List α} : cyclicPermutations l = cyclicPermutations l' ↔ l = l' :=
  cyclicPermutations_injective.eq_iff

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