mul_right

Mathlib.Data.PNat.Prime

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

← MathLib Explorer

English

Let k, m, n be positive integers. If gcd(k,m)=1 and gcd(k,n)=1, then gcd(k, m n)=1.

Русский

Пусть k, m, n — положительные целые. Если gcd(k, m)=1 и gcd(k, n)=1, то gcd(k, m n)=1.

LaTeX

$$$ (gcd(k,m)=1 \,\wedge\, gcd(k,n)=1) \rightarrow gcd(k, m n)=1 $$$

Lean4

theorem mul_right {k m n : ℕ+} : k.Coprime m → k.Coprime n → k.Coprime (m * n) :=
  by
  repeat rw [← coprime_coe]
  rw [mul_coe]
  apply Nat.Coprime.mul_right

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

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

Разделы

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

Аффилиация

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