int_gcd_helper'

Mathlib.Tactic.NormNum.GCD

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.int_gcd_helper'

Lean4

theorem int_gcd_helper' {d : ℕ} {x y : ℤ} (a b : ℤ) (h₁ : (d : ℤ) ∣ x) (h₂ : (d : ℤ) ∣ y) (h₃ : x * a + y * b = d) :
    Int.gcd x y = d :=
  by
  refine Nat.dvd_antisymm ?_ (Int.natCast_dvd_natCast.1 (Int.dvd_coe_gcd h₁ h₂))
  rw [← Int.natCast_dvd_natCast, ← h₃]
  apply dvd_add
  · exact (Int.gcd_dvd_left ..).mul_right _
  · exact (Int.gcd_dvd_right ..).mul_right _

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

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

Разделы

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

Аффилиация

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