support_finRotate

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#support_finRotate

English

The support of finRotate(n+2) is the full set of indices: it moves every element.

Русский

Опора перестановки finRotate(n+2) равна всем индексам; каждый элемент перемещается.

LaTeX

$$$ \\operatorname{supp}(\\mathrm{finRotate}(n+2)) = \\operatorname{Finset.univ}$$$

Lean4

@[simp]
theorem support_finRotate {n : ℕ} : support (finRotate (n + 2)) = Finset.univ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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