Sum of three cubes

An integer n : ℤ can be written as a sum of three cubes (of integers) if and only if n is not 4 or 5 mod 9.

References:

• Wikipedia
• mathoverflow/100324 asked by user David Feldman

def SumOfThreeCubes.IsSumOfThreeCubes {R : Type u_1} [Ring R] (n : R) : Prop

The predicate that n : R is a sum of three cubes.

Equations

• SumOfThreeCubes.IsSumOfThreeCubes n = ∃ (x : R) (y : R) (z : R), n = x ^ 3 + y ^ 3 + z ^ 3

theorem SumOfThreeCubes.isSumOfThreeCubes_2 : IsSumOfThreeCubes 2

theorem SumOfThreeCubes.isSumOfThreeCubes_33 : IsSumOfThreeCubes 33

theorem SumOfThreeCubes.isSumOfThreeCubes_42 : IsSumOfThreeCubes 42

theorem SumOfThreeCubes.mod_9_of_isSumOfThreeCubes (n : ℤ) (hn : IsSumOfThreeCubes n) : ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])

theorem SumOfThreeCubes.isSumOfThreeCubesRat_any (r : ℚ) : IsSumOfThreeCubes r

Any rational number is a sum of three rational cubes.

First proved by Ryley in 1825, which can be found in [Ri1930]. The below parametrization is brought from the MSE answer [MSE].

[Ri1930] Richmond, H. W. "On Rational Solutions of $x^3 + y^3 + z^3 = R$." Proceedings of the Edinburgh Mathematical Society 2.2 (1930): 92-100. [MSE] Kieren MacMillan, Proving that any rational number can be represented as the sum of the cubes of three rational numbers, https://math.stackexchange.com/q/4480969

theorem SumOfThreeCubes.isSumOfThreeCubes_iff_mod_9 : (∀ (n : ℤ), IsSumOfThreeCubes n ↔ ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])) ↔ sorry

An integer n : ℤ can be written as a sum of three cubes (of integers) if and only if n is not 4 or 5 mod 9.