lean_workbook_plus_23347
ProvedFind the least common multiple (lcm) of two numbers and given that their greatest common divisor (gcd) is 13 and their product is 897.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23347 (a b : ℕ) (h1 : Nat.gcd a b = 13) (h2 : a * b = 897) : Nat.lcm a b = 69 := by sorry
Source