instCircularOrderFin

Mathlib.Order.Circular.ZMod

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

English

For every natural n, there is a circular order on Fin(n).

Русский

Для каждого натурального n существует циклический порядок на Fin(n).

LaTeX

$$$ \\forall n \\in \\mathbb{N}, \\; \\text{CircularOrder}(\\mathrm{Fin}(n)) $$$

Lean4

instance (n : ℕ) : CircularOrder (Fin n) :=
  LinearOrder.toCircularOrder _

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

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

Разделы

Аффилиация

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