gcd_mul

Mathlib.Data.PNat.Prime

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

← MathLib Explorer

English

If gcd(m,n)=1, then gcd(k, m n) = gcd(k,m) gcd(k,n).

Русский

Если gcd(m,n)=1, то gcd(k, m n) = gcd(k,m) gcd(k,n).

LaTeX

$$$ \gcd(k, m n) = \gcd(k,m) \gcd(k,n) \text{, при } \gcd(m,n)=1 $$$

Lean4

theorem gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.Coprime n) : k.gcd (m * n) = k.gcd m * k.gcd n :=
  by
  rw [← coprime_coe] at h; apply eq
  simp only [gcd_coe, mul_coe]; apply Nat.Coprime.gcd_mul k h

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

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

Разделы

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

Аффилиация

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