finRotate_one

Mathlib.Logic.Equiv.Fin.Rotate

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

English

finRotate(1) is the identity permutation.

Русский

finRotate(1) — перестановка-тождество.

LaTeX

$$$\\mathrm{finRotate}(1) = \\mathrm{Equiv.refl}(\\mathrm{Fin}(1))$$$

Lean4

@[simp]
theorem finRotate_one : finRotate 1 = Equiv.refl _ :=
  Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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