cyclicPermutations_injective — Mathlib

English

The function l ↦ cyclicPermutations(l) is injective: if cyclicPermutations(l) = cyclicPermutations(l'), then l = l'.

Русский

Функция l ↦ cyclicPermutations(l) инъективна: если cyclicPermutations(l) = cyclicPermutations(l'), то l = l'.

LaTeX

$$$ \forall l,l',\; \text{cyclicPermutations}(l) = \text{cyclicPermutations}(l') \Rightarrow l = l' $$$

Lean4

theorem cyclicPermutations_injective : Function.Injective (@cyclicPermutations α) := fun l l' h ↦ by
  simpa using congr_arg head? h

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