mod_four_ne_three_of_sq_eq_neg_sq

Mathlib.NumberTheory.LegendreSymbol.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.mod_four_ne_three_of_sq_eq_neg_sq

← MathLib Explorer

English

If x ≠ 0 and x^2 ≡ -y^2 (mod p), then p ≡ 1 (mod 4).

Русский

Если x ≠ 0 и x^2 ≡ -y^2 (mod p), тогда p ≡ 1 (mod 4).

LaTeX

$$$x \neq 0 \text{ and } x^2 \equiv -y^2 \pmod{p} \Rightarrow p \equiv 1 \pmod{4}$$$

Lean4

theorem mod_four_ne_three_of_sq_eq_neg_sq {x y : ZMod p} (hx : x ≠ 0) (hxy : x ^ 2 = -y ^ 2) : p % 4 ≠ 3 :=
  mod_four_ne_three_of_sq_eq_neg_sq' hx (neg_eq_iff_eq_neg.mpr hxy).symm

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

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

Разделы

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

Аффилиация

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