mul_div_exact — Mathlib

English

If m,k ∈ ℕ⁺ and k ∣ m, then k × divExact m k = m.

Русский

Если m,k ∈ ℕ⁺ и k делит m, то k умножить на divExact m k равно m.

LaTeX

$$$$ \forall {m,k \in \mathbb{N}_{>0}}, (k \mid m) \Rightarrow k \cdot \operatorname{divExact}(m,k) = m $$$$

Lean4

theorem mul_div_exact {m k : ℕ+} (h : k ∣ m) : k * divExact m k = m :=
  by
  apply PNat.eq; rw [mul_coe]
  change (k : ℕ) * (div m k).succ = m
  rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]

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