dvd_gcd

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.dvd_gcd

← MathLib Explorer

English

If c divides a and c divides b, then c divides gcd(a,b).

Русский

Если c делит a и c делит b, то c делит gcd(a,b).

LaTeX

$$$ c \mid a \rightarrow c \mid b \rightarrow c \mid \gcd\,a\,b $$$

Lean4

theorem dvd_gcd {a b c : R} : c ∣ a → c ∣ b → c ∣ gcd a b :=
  GCD.induction a b (fun _ _ H => by simpa only [gcd_zero_left] using H) fun a b _ IH ca cb =>
    by
    rw [gcd_val]
    exact IH ((dvd_mod_iff ca).2 cb) ca

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

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

Разделы

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

Аффилиация

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