gcd_eq_one_of_gcd_mul_right_eq_one_left

Mathlib.Data.Int.GCD

URI: https://scilib.ai/kg/mathlib#Int.gcd_eq_one_of_gcd_mul_right_eq_one_left

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$a \\mid bc \\wedge \\gcd(a,c) = 1 \\Rightarrow a \\mid b.$$$$

Lean4

/-- If `gcd a (m * n) = 1`, then `gcd a m = 1`. -/
theorem gcd_eq_one_of_gcd_mul_right_eq_one_left {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) : a.gcd m = 1 :=
  Nat.dvd_one.mp <| h ▸ gcd_dvd_gcd_mul_right_right a m n

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

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

Разделы

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

Аффилиация

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