mul_div_mul_comm_of_dvd_dvd — Mathlib

English

gcd x y · lcm x y = x · y ( повторение).

Русский

gcd x y · lcm x y = x · y (повторение).

LaTeX

$$$\gcd(x,y) \cdot \operatorname{lcm}(x,y) = x \cdot y$$$

Lean4

theorem mul_div_mul_comm_of_dvd_dvd {a b c d : R} (hac : c ∣ a) (hbd : d ∣ b) : a * b / (c * d) = a / c * (b / d) :=
  by
  rcases eq_or_ne c 0 with (rfl | hc0); · simp
  rcases eq_or_ne d 0 with (rfl | hd0); · simp
  obtain ⟨k1, rfl⟩ := hac
  obtain ⟨k2, rfl⟩ := hbd
  rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]

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