finRotate_last

Mathlib.Logic.Equiv.Fin.Rotate

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

English

finRotate(n+1)(Fin.last n) = 0.

Русский

finRotate(n+1)(Fin.last n) = 0.

LaTeX

$$$\\mathrm{finRotate}(n+1)(\\mathrm{Fin.last}\\ n) = 0$$$

Lean4

theorem finRotate_last : finRotate (n + 1) (Fin.last _) = 0 :=
  finRotate_last'

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

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

Разделы

Аффилиация

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