Commit 2025-07-15 10:52 b330acfb

feat: coin problem with two coins and prime ideals in ℕ (#27065) This is the outcome of a course project at Heidelberg University: https://matematiflo.github.io/CompAssistedMath2025/

• If the gcd of two natural numbers p and q divides a third natural number n, and if n is at least (p - 1) * (q - 1), then n can be represented as an ℕ-linear combination of p and q; in other words, one can pay the amount n using coins of value p and q.
• As a consequence, the prime ideals in ℕ are 0, ⟨p⟩, and {1}ᶜ.