div_dvd_div_left

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.div_dvd_div_left

English

If m|k and n|m, then (k/m) divides (k/n).

Русский

Если m делит k и n делит m, то (k/m) делит (k/n).

LaTeX

$$$\forall n,m,k \in \mathbb{N}, (m \mid k) \land (n \mid m) \Rightarrow (k / m) \mid (k / n)$$$

Lean4

theorem div_dvd_div_left (hkm : m ∣ k) (hkn : n ∣ m) : k / m ∣ k / n :=
  ⟨_, (div_mul_div hkm hkn).symm⟩

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

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

Разделы

Аффилиация

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