χ₈'_nat_eq_if_mod_eight — Mathlib

English

An explicit description of χ8' on natural numbers: χ8'(n) = 0 if n is even; if n is odd, χ8'(n) = 1 when n ≡ 1 or 3 (mod 8), and −1 otherwise.

Русский

Явное описание χ8' на натуральных числах: χ8'(n) = 0, если n чётно; иначе χ8'(n) = 1, если n ≡ 1 или 3 (mod 8), иначе −1.

LaTeX

$$$$\chi_8'(n)=\begin{cases}0,& 2|n,\\[2pt]1,& n\equiv 1,3 \pmod{8},\\[2pt]-1,& \text{иначе } n\equiv 5,7 \pmod{8}.\end{cases}$$$$

Lean4

theorem χ₈'_nat_eq_if_mod_eight (n : ℕ) : χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 :=
  mod_cast χ₈'_int_eq_if_mod_eight n

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