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, then r^2 + s^2 is coprime to rs.

Русский

Если $\gcd(r,s)=1$, то $\gcd(r^2+s^2, rs)=1$.

LaTeX

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

Lean4

theorem isCoprime_of_sq_sum' {r s : ℤ} (h : IsCoprime r s) : IsCoprime (r ^ 2 + s ^ 2) (r * s) :=
  by
  apply IsCoprime.mul_right (Int.isCoprime_of_sq_sum (isCoprime_comm.mp h))
  rw [add_comm]; apply Int.isCoprime_of_sq_sum h

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

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

Разделы

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

Аффилиация

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