English
For divisors m|k and n|k, (k/m) lcm (k/n) equals k/(m gcd n).
Русский
Для делителей m|k и n|k, (k/m) lcm (k/n) равно k/(m gcd n).
LaTeX
$$$\forall {n,m,k} \in \mathbb{N}, (m \mid k) \land (n \mid k) \Rightarrow (k / m) \operatorname{lcm}(k / n) = k / (m \gcd n)$$$
Lean4
theorem div_lcm_eq_div_gcd (hkm : m ∣ k) (hkn : n ∣ k) : (k / m).lcm (k / n) = k / (m.gcd n) :=
by
rw [Nat.lcm_eq_iff]
refine ⟨div_dvd_div_left hkm (Nat.gcd_dvd_left m n), div_dvd_div_left hkn (Nat.gcd_dvd_right m n), fun c hmc hnc ↦ ?_⟩
rcases m.eq_zero_or_pos with hm | hm
· simp_all
rcases n.eq_zero_or_pos with hn | hn
· simp_all
rw [Nat.div_dvd_iff_dvd_mul hkm hm] at hmc
rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc
simpa [Nat.div_dvd_iff_dvd_mul (Nat.dvd_trans (Nat.gcd_dvd_left m n) hkm) (gcd_pos_of_pos_left n hm),
Nat.gcd_mul_right m c n] using (Nat.dvd_gcd hmc hnc)
