isCoprime_of_sq_sum

Mathlib.NumberTheory.FLT.Four

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

← MathLib Explorer

English

If r and s are coprime integers, then r^2 + s^2 is coprime to r.

Русский

Если r и s — взаимно простые целые, то gcd(r^2 + s^2, r) = 1.

LaTeX

$$$\gcd(r^2 + s^2, r) = 1$ whenever $\gcd(r,s)=1$$$

Lean4

theorem isCoprime_of_sq_sum {r s : ℤ} (h2 : IsCoprime s r) : IsCoprime (r ^ 2 + s ^ 2) r :=
  by
  rw [sq, sq]
  exact (IsCoprime.mul_left h2 h2).mul_add_left_left r

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

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

Разделы

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

Аффилиация

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