`triangular_formula`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.PhysicalMotivation on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  77def triangular (n : ℕ) : ℕ := n * (n + 1) / 2
  78
  79/-- Triangular number formula. -/
  80theorem triangular_formula (n : ℕ) : triangular n = n * (n + 1) / 2 := rfl
  81
  82/-- Recursive definition of triangular numbers.
  83    We verify this by direct computation for specific values. -/
  84theorem triangular_rec_at_8 : triangular 9 = triangular 8 + 9 := by rfl
  85
  86/-- T(0) = 0. -/
  87@[simp] lemma triangular_0 : triangular 0 = 0 := rfl
  88
  89/-- T(1) = 1. -/
  90@[simp] lemma triangular_1 : triangular 1 = 1 := rfl
  91
  92/-- T(2) = 3. -/
  93@[simp] lemma triangular_2 : triangular 2 = 3 := rfl
  94
  95/-- T(3) = 6. -/
  96@[simp] lemma triangular_3 : triangular 3 = 6 := rfl
  97
  98/-- T(4) = 10. -/
  99@[simp] lemma triangular_4 : triangular 4 = 10 := rfl
 100
 101/-- T(5) = 15. -/
 102@[simp] lemma triangular_5 : triangular 5 = 15 := rfl
 103
 104/-- T(8) = 36. -/
 105@[simp] lemma triangular_8 : triangular 8 = 36 := rfl
 106
 107/-- **KEY RESULT**: T(9) = 45. -/
 108@[simp] theorem triangular_9_is_45 : triangular 9 = 45 := rfl
 109
 110/-! ## The Closure Principle -/

papers checked against this theorem

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