lean_workbook_plus_51586
Provedmod for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51586 (n : ℕ) (i : ℕ) (hi : i ≤ (n-1)/2) : (n*i + 2*i + 1) % (n+1) = (i + 1) % (n+1) := by sorry
Source
mod for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_51586 (n : ℕ) (i : ℕ) (hi : i ≤ (n-1)/2) : (n*i + 2*i + 1) % (n+1) = (i + 1) % (n+1) := by sorry