Enlargements of schemes

Lars Brünjes and Christian Serpé

def φ₀ (p : ℕ) : Prop

Equations

• φ₀ p = ((2 + 0) % p = 0 % p)

theorem proof_of_concept : ¬∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → (φ₀ p ↔ φ₀ q)

def ψ (p : ℕ) (x : ℕ) : Prop

Equations

• ψ p x = (x * x % p = 2 % p)

theorem sqrt_mod2 : ∃ (x : ℕ), ψ 2 x

theorem sqrt_mod3 : ¬∃ (x : ℕ), ψ 3 x