gcd_dvd_gcd

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#gcd_dvd_gcd

← MathLib Explorer

English

If a | b and c | d, then gcd a c divides gcd b d.

Русский

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

LaTeX

$$$$ \text{If } a \mid b \text{ and } c \mid d, \text{ then } \gcd(a,c) \mid \gcd(b,d). $$$$

Lean4

@[gcongr]
theorem gcd_dvd_gcd [GCDMonoid α] {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d :=
  dvd_gcd ((gcd_dvd_left _ _).trans hab) ((gcd_dvd_right _ _).trans hcd)

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

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

Разделы

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

Аффилиация

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