`lcm_8_45_eq_360`

proved

show as: view math explainer →

module: IndisputableMonolith.Gap45
domain: Gap45
line: 18 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gap45 on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  15@[simp] lemma gcd_8_45_eq_one : Nat.gcd 8 45 = 1 := by decide
  16
  17/-- lcm(8,45) = 360. -/
  18lemma lcm_8_45_eq_360 : Nat.lcm 8 45 = 360 := by
  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. -/
  26lemma lcm_8_45_div_8 : Nat.lcm 8 45 / 8 = 45 := by
  27  have h := lcm_8_45_eq_360
  28  have : 360 / 8 = 45 := by decide
  29  simpa [h] using this
  30
  31/-- Exact cycle counts: lcm(8,45)/45 = 8. -/
  32lemma lcm_8_45_div_45 : Nat.lcm 8 45 / 45 = 8 := by
  33  have h := lcm_8_45_eq_360
  34  have : 360 / 45 = 8 := by decide
  35  simpa [h] using this
  36
  37/-- lcm(9,5) = 45, characterizing the first simultaneous occurrence of 9- and 5-fold periodicities. -/
  38lemma lcm_9_5_eq_45 : Nat.lcm 9 5 = 45 := by
  39  have hg : Nat.gcd 9 5 = 1 := by decide
  40  have h := Nat.gcd_mul_lcm 9 5
  41  have h' : Nat.lcm 9 5 = 9 * 5 := by simpa [hg, Nat.one_mul] using h
  42  have hmul : 9 * 5 = 45 := by decide
  43  simpa [hmul] using h'
  44
  45/-- 9 ∣ 45. -/
  46@[simp] lemma nine_dvd_45 : 9 ∣ 45 := by exact ⟨5, by decide⟩
  47
  48/-- 5 ∣ 45. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.