factor_eq_gcd_right

Mathlib.Data.PNat.Prime

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

← MathLib Explorer

English

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

Русский

Пусть gcd(m,n)=1, a|m, b|n. Тогда gcd(m, a b) = a.

LaTeX

$$$ \gcd(m, a b) = a \quad\text{при}\quad \gcd(m,n)=1, \ a|m, \ b|n $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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