perm

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.IsRotated.perm

English

If l is a rotation of l', then l is a permutation of l'.

Русский

Если l является вращением l', то l является перестановкой l'.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \Rightarrow l \Perm l' $$$

Lean4

theorem perm (h : l ~r l') : l ~ l' :=
  Exists.elim h fun _ hl => hl ▸ (rotate_perm _ _).symm

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

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

Разделы

Аффилиация

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