factor_eq_gcd_right_right

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.Coprime.factor_eq_gcd_right_right

← MathLib Explorer

English

If cop = gcd(m,n)=1 and a|m, b|n, then a = gcd(m, b a).

Русский

Если gcd(m,n)=1 и a|m, b|n, тогда a = gcd(m, b a).

LaTeX

$$$ a = gcd(m, b a) $$$

Lean4

theorem factor_eq_gcd_right_right {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m) (bn : b ∣ n) : a = m.gcd (b * a) :=
  by
  rw [gcd_comm]
  apply Coprime.factor_eq_gcd_right cop am bn

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

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

Разделы

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

Аффилиация

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