Sum_of_Odd_Positive_Powers

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

divisibilitynumber-theoryproofwiki

Let $n \in \N$ be an odd positive integer. Let $x, y \in \Z_{>0}$ be (strictly) positive integers. Then $x + y$ is a divisor of $x^n + y^n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Sum_of_Odd_Positive_Powers (n : ℕ) (hn : Odd n) (x y : ℤ) : (x + y) ∣ (x ^ n + y ^ n) := by sorry

Source