lean_workbook_plus_53094
ProvedIf is odd, then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53094 (n : ℕ) : n % 2 = 1 → 5 ∣ 1 ^ n + 4 ^ n ∧ 5 ∣ 2 ^ n + 3 ^ n := by sorry
Source
If is odd, then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_53094 (n : ℕ) : n % 2 = 1 → 5 ∣ 1 ^ n + 4 ^ n ∧ 5 ∣ 2 ^ n + 3 ^ n := by sorry