lean_workbook_plus_64938
ProvedGiven and , prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64938 (n : ℕ) (hn : n ≠ 0) : 2 * (n * (n + 1) / 2) / (n * (n + 1) / 2) = 2 := by sorry
Source
Given and , prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_64938 (n : ℕ) (hn : n ≠ 0) : 2 * (n * (n + 1) / 2) / (n * (n + 1) / 2) = 2 := by sorry