isQuadratic_χ₄

Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

English

χ₄(n) depends only on n mod 4 for natural n.

Русский

χ₄(n) зависит только от n mod 4 для натуральных n.

LaTeX

$$$ χ_{4}(n) = χ_{4}(n \\bmod 4) $ for all natural n. $$

Lean4

/-- `χ₄` takes values in `{0, 1, -1}` -/
theorem isQuadratic_χ₄ : χ₄.IsQuadratic := by
  unfold MulChar.IsQuadratic
  decide

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

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

Разделы

Аффилиация

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