pith. machine review for the scientific record. sign in
lemma proved tactic proof

lcm_8_45_eq_360

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  18lemma lcm_8_45_eq_360 : Nat.lcm 8 45 = 360 := by

proof body

Tactic-mode proof.

  19  have hg : Nat.gcd 8 45 = 1 := by decide
  20  have h := Nat.gcd_mul_lcm 8 45
  21  have : Nat.lcm 8 45 = 8 * 45 := by simpa [hg, Nat.one_mul] using h
  22  have hm : 8 * 45 = 360 := by decide
  23  exact this.trans hm
  24
  25/-- Exact cycle counts: lcm(8,45)/8 = 45. -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.