eq_neg_one_iff'

Mathlib.NumberTheory.LegendreSymbol.Basic

URI: https://scilib.ai/kg/mathlib#legendreSym.eq_neg_one_iff'

English

For natural a with a ≠ 0 mod p, legendreSym p a = -1 iff not IsSquare a.cast.

Русский

Для натурала a с a ≠ 0 (mod p) legendreSym p a = -1 тогда и только тогда, когда a.cast не является квадратом.

LaTeX

$$$\mathrm{legendreSym}(p, a) = -1 \iff \lnot IsSquare (a \bmod p)$$$

Lean4

theorem eq_neg_one_iff' {a : ℕ} : legendreSym p a = -1 ↔ ¬IsSquare (a : ZMod p) := by rw [eq_neg_one_iff]; norm_cast

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

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

Разделы

Аффилиация

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