instCircularOrderZMod — Mathlib

English

There is a circular order on ZMod n for every natural n, defined inductively via ℤ for n=0 and via Fin(n+1) for n≥0.

Русский

Для каждого натурального n существует циклический порядок на ZMod(n), определяемый индуктивно: для n=0 берём ℤ, а для n≥0 — Fin(n+1).

LaTeX

$$$ \\forall n \\in \\mathbb{N}, \\; \\text{CircularOrder}(\\mathbb{Z}/n\\mathbb{Z}) $$$

Lean4

instance : ∀ (n : ℕ), CircularOrder (ZMod n)
  | 0 => inferInstanceAs <| CircularOrder ℤ
  | n + 1 => inferInstanceAs <| CircularOrder <| Fin <| n + 1

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