length_rotate

Mathlib.Data.List.Rotate

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

English

The operation rotate preserves length: length(l.rotate n) = length(l).

Русский

Операция вращения сохраняет длину: length(l.rotate n) = length(l).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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