div_mul_div — Mathlib

English

If m divides k and n divides 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_mul_div (hkm : m ∣ k) (hkn : n ∣ m) : (k / m) * (m / n) = k / n :=
  by
  rcases n.eq_zero_or_pos with hn | hn
  · simp [hn]
  refine (Nat.div_eq_of_eq_mul_left hn ?_).symm
  rw [mul_assoc, Nat.div_mul_cancel hkn, Nat.div_mul_cancel hkm]

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