dvd_mul_right

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Coprime.dvd_mul_right

English

If k and n are coprime, then k | m·n iff k | m.

Русский

Если k и n взаимно просты, то k делит произведение m·n тогда и только тогда, когда k делит m.

LaTeX

$$$\text{Coprime}(k,n) \Rightarrow (k \mid m n \iff k \mid m).$$$

Lean4

theorem dvd_mul_right {m n k : ℕ} (H : Coprime k n) : k ∣ m * n ↔ k ∣ m :=
  ⟨H.dvd_of_dvd_mul_right, fun h => dvd_mul_of_dvd_left h n⟩

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

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

Разделы

Аффилиация

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