nodup_rotate

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.nodup_rotate

English

Rotation preserves the property of being nodup: Nodup(l.rotate n) ↔ Nodup(l).

Русский

Вращение сохраняет свойство ненадо: Nodup(l.rotate n) ↔ Nodup(l).

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\forall l \\in \\mathsf{List}(\\alpha),\\ Nodup(l.rotate n) \\Leftrightarrow Nodup(l)$$$

Lean4

@[simp]
theorem nodup_rotate {l : List α} {n : ℕ} : Nodup (l.rotate n) ↔ Nodup l :=
  (rotate_perm l n).nodup_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru