at_one

Mathlib.NumberTheory.LegendreSymbol.Basic

URI: https://scilib.ai/kg/mathlib#legendreSym.at_one

English

For odd prime p, the number of solutions x modulo p to x^2 ≡ a is 1 + legendreSym p a.

Русский

Для нечётного простого p число решений уравнения x^2 ≡ a по модулю p равно 1 + legendreSym p a.

LaTeX

$$$\#\{x \in \mathbb{Z}/p\mathbb{Z} : x^2 \equiv a\} = \mathrm{legendreSym}(p,a) + 1\quad (p \neq 2)$$$

Lean4

@[simp]
theorem at_one : legendreSym p 1 = 1 := by rw [legendreSym, Int.cast_one, MulChar.map_one]

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

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

Разделы

Аффилиация

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