eq_one_or_neg_one

Mathlib.NumberTheory.LegendreSymbol.Basic

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

← MathLib Explorer

English

If p ∤ a, then legendreSym p a ∈ {1, -1}.

Русский

Если p не делит a, то legendreSym p a ∈ {1, -1}.

LaTeX

$$$\big(\mathrm{legendreSym}(p,a) = 1\big) \lor \big(\mathrm{legendreSym}(p,a) = -1\big)$, когда $(a\bmod p) \neq 0$$$

Lean4

/-- If `p ∤ a`, then `legendreSym p a` is `1` or `-1`. -/
theorem eq_one_or_neg_one {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p a = 1 ∨ legendreSym p a = -1 :=
  quadraticChar_dichotomy ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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