rotate_length

Mathlib.Data.List.Rotate

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

English

Rotation preserves length: the length of l.rotate n equals the length of l.

Русский

Вращение сохраняет длину: длина l.rotate n равна длине l.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\forall l \\in \\mathsf{List}(\\alpha),\\ \\operatorname{length}(l.rotate n) = \\operatorname{length}(l)$$$

Lean4

@[simp]
theorem rotate_length (l : List α) : rotate l l.length = l := by rw [rotate_eq_rotate', rotate'_length]

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

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

Разделы

Аффилиация

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