dvd_lcm_left — Mathlib

English

x divides the least common multiple of x and y.

Русский

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

LaTeX

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

Lean4

theorem dvd_lcm_left (x y : R) : x ∣ 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).2
    ⟨z, Eq.symm <| eq_div_of_mul_eq_left hxy <| by rw [mul_right_comm, mul_assoc, ← hz]⟩

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