sq_ne_two_mod_four

Mathlib.NumberTheory.PythagoreanTriples

URI: https://scilib.ai/kg/mathlib#Int.sq_ne_two_mod_four

← MathLib Explorer

English

For any integer z, z^2 is not congruent to 2 modulo 4.

Русский

Для любого целого z квадрат не конгруентен к 2 по модулю 4.

LaTeX

$$$z^2 \not\equiv 2 \pmod{4}$$$

Lean4

theorem sq_ne_two_mod_four (z : ℤ) : z * z % 4 ≠ 2 :=
  by
  suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact this
  rw [← ZMod.intCast_eq_intCast_iff']
  simpa using sq_ne_two_fin_zmod_four _

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

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

Разделы

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

Аффилиация

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