gcd_eq

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.ModEq.gcd_eq

← MathLib Explorer

English

If a ≡ b (mod m), then gcd(a,m) = gcd(b,m).

Русский

Если a ≡ b (mod m), то gcd(a,m) = gcd(b,m).

LaTeX

$$$ a \equiv b \pmod{m} \Rightarrow \gcd(a,m) = \gcd(b,m) $$$

Lean4

theorem gcd_eq (h : a ≡ b [MOD m]) : gcd a m = gcd b m :=
  by
  have h1 := gcd_dvd_right a m
  have h2 := gcd_dvd_right b m
  exact
    dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
      (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

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

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

Разделы

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

Аффилиация

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