Existence_of_Lowest_Common_Multiple

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lowest-common-multipleproofwiki

Let a, b be integers with ab ≠ 0. Then their lowest common multiple exists.

Preamble

import Mathlib.Data.Int.GCD

Formal statement

theorem Existence_of_Lowest_Common_Multiple (a b : ℤ) (h : a * b ≠ 0) : ∃ m : ℤ, m > 0 ∧ a ∣ m ∧ b ∣ m ∧ ∀ n : ℤ, a ∣ n → b ∣ n → m ∣ n := by sorry

Source