mod_four_ne_three_of_sq_eq_neg_one

Mathlib.NumberTheory.LegendreSymbol.Basic

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

English

If there exists y with y^2 ≡ -1 (mod p), then p ≡ 1 (mod 4).

Русский

Если существует y такая, что y^2 ≡ -1 (mod p), то p ≡ 1 (mod 4).

LaTeX

$$$\exists y:\; y^2 \equiv -1 \pmod{p} \Rightarrow p \equiv 1 \pmod{4}$$$

Lean4

theorem mod_four_ne_three_of_sq_eq_neg_one {y : ZMod p} (hy : y ^ 2 = -1) : p % 4 ≠ 3 :=
  exists_sq_eq_neg_one_iff.1 ⟨y, hy ▸ pow_two y⟩

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

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

Разделы

Аффилиация

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