lean_workbook_plus_44891
OpenAmong positive integers less than or equal to 2011, denote the sum of the integers which have remainder of 1 when divided by 3 and denote for remainder of 2. Find the value of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44891 (A B : ℕ) (hA : A = ∑ i in Finset.filter (λ x => x % 3 = 1) (Finset.Icc 1 2011), i) (hB : B = ∑ i in Finset.filter (λ x => x % 3 = 2) (Finset.Icc 1 2011), i) : A - B = 1341 := by sorry
Source