dvd_lcm_right — Mathlib

English

y divides the least common multiple of x and y.

Русский

y делится на наименьшее общее кратное x и y.

LaTeX

$$$y \mid \operatorname{lcm}(x,y)$$$

Lean4

theorem dvd_lcm_right (x y : R) : y ∣ lcm x y :=
  by_cases
    (fun hxy : gcd x y = 0 => by
      rw [lcm, hxy, div_zero]
      exact dvd_zero _)
    fun hxy =>
    let ⟨z, hz⟩ := (gcd_dvd x y).1
    ⟨z, Eq.symm <| eq_div_of_mul_eq_right hxy <| by rw [← mul_assoc, mul_right_comm, ← hz]⟩

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