lcm_dvd — Mathlib

English

If m | k and n | k for positive integers m, n, k, then lcm(m, n) divides k.

Русский

Если m делит k и n делит k для положительных m, n, k, то lcm(m, n) делит k.

LaTeX

$$$ (m \\mid k) \\\\land (n \\mid k) \\\\Rightarrow \\operatorname{lcm}(m,n) \\mid k $$$

Lean4

theorem lcm_dvd {m n k : ℕ+} (hm : m ∣ k) (hn : n ∣ k) : lcm m n ∣ k :=
  dvd_iff.2 (@Nat.lcm_dvd (m : ℕ) (n : ℕ) (k : ℕ) (dvd_iff.1 hm) (dvd_iff.1 hn))

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