Weak Goldbach for prime : singleton prime multiset
OpenWeakGoldbach.three_primes_of_primegoldbachnumber-theoryweak-goldbach
Every prime is the sum of at most three primes: the singleton multiset has cardinality , its only member is prime by hypothesis, and its sum is . This generalizes the small cases and of the weak Goldbach mission.
Preamble
import Mathlib set_option autoImplicit false
Formal statement
theorem WeakGoldbach.three_primes_of_prime (p : ℕ) (hp : Nat.Prime p) :
∃ s : Multiset ℕ, s.card ≤ 3 ∧ (∀ q ∈ s, Nat.Prime q) ∧ s.sum = p := by sorry