`triangular`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.PhysicalMotivation on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  74/-! ## Triangular Numbers -/
  75
  76/-- The n-th triangular number: T(n) = 1 + 2 + ... + n = n(n+1)/2. -/
  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. -/

papers checked against this theorem

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