lean_workbook_plus_19229

Proved

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

The greatest common divisor of $n$ and $180$ is $12$ . The least common multiple of $n$ and $180$ is $720$ . Find $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19229 (n : ℕ) (h1 : Nat.gcd n 180 = 12) (h2 : Nat.lcm n 180 = 720) : n = 48   :=  by sorry

Source