χ₄_nat_eq_if_mod_four

Mathlib.NumberTheory.LegendreSymbol.ZModChar

URI: https://scilib.ai/kg/mathlib#ZMod.χ₄_nat_eq_if_mod_four

English

Same explicit piecewise formula for natural n as above.

Русский

Та же явная кусочно-заданная формула для натурального n.

LaTeX

$$$ χ_{4}(n) = \\begin{cases}0,& n \\equiv 0 \\pmod{2} \\\\ 1,& n \\equiv 1 \\pmod{4} \\\\ -1,& n \\equiv 3 \\pmod{4} \\end{cases}$$$

Lean4

theorem χ₄_nat_eq_if_mod_four (n : ℕ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
  mod_cast χ₄_int_eq_if_mod_four n

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

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

Разделы

Аффилиация

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