dvd_mul_left

Mathlib.Data.Nat.GCD.Basic

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

English

If H is Coprime k m, then k | m·n iff k | n.

Русский

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

LaTeX

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

Lean4

theorem dvd_mul_left {m n k : ℕ} (H : Coprime k m) : k ∣ m * n ↔ k ∣ n :=
  ⟨H.dvd_of_dvd_mul_left, fun h => dvd_mul_of_dvd_right h m⟩

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

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

Разделы

Аффилиация

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