English
Let α be a gcd monoid. Then the least common multiple of a and b divides c if and only if a divides c and b divides c.
Русский
Пусть α – gcd-монойд. Тогда НОК(a,b) делит c тогда и только тогда, когда a делит c и b делит c.
LaTeX
$$$ \operatorname{lcm}(a,b) \mid c \iff a \mid c \land b \mid c $$$
Lean4
theorem lcm_dvd_iff [GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
by
by_cases h : a = 0 ∨ b = 0
·
rcases h with (rfl | rfl) <;>
simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right, zero_dvd_iff, dvd_zero, and_true, imp_true_iff]
· obtain ⟨h1, h2⟩ := not_or.1 h
have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ← (gcd_mul_right' c a b).dvd_iff_dvd_right,
dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1, mul_dvd_mul_iff_right h2, and_comm]
