def Goldbach.IsGoldbachPair (n p q : ℕ) : Prop

A pair of primes (p, q) is a Goldbach decomposition of n when p + q = n.

Equations

• Goldbach.IsGoldbachPair n p q = (Nat.Prime p ∧ Nat.Prime q ∧ p + q = n)

def Goldbach.HasGoldbachDecomposition (n : ℕ) : Prop

n satisfies the strong Goldbach property when it has a prime-sum decomposition.

Equations

• Goldbach.HasGoldbachDecomposition n = ∃ (p : ℕ), ∃ (q : ℕ), Goldbach.IsGoldbachPair n p q