isQuadratic_χ₈

Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

English

The function χ₈ is a quadratic character (values in {0,1,-1}).

Русский

Функция χ₈ является квадратичным символом (значения в {0,1,-1}).

LaTeX

$$$ χ_{8}^2(a) \\in \\{0,1\\} \\text{ and } χ_{8}(a) \\in \\{0,1,-1\\}. $$$

Lean4

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

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

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

Разделы

Аффилиация

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