lean_workbook_plus_71643
ProvedProve that divides both and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71643 (a : ℕ) : 3 ∣ (a-2)*(a-1)*a ∧ 3 ∣ a*(a+1)*(a+2) := by sorry
Source
Prove that divides both and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71643 (a : ℕ) : 3 ∣ (a-2)*(a-1)*a ∧ 3 ∣ a*(a+1)*(a+2) := by sorry