theorem proved term proof

`lcm_fortyfive_eighthundredforty`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 715theorem lcm_fortyfive_eighthundredforty : Nat.lcm 45 840 = 2520 := by native_decide

Term-mode proof.

 716
 717/-- lcm(360, 840) = 2520. -/