Quadratic Residue Exercise

Find all prime numbers $p$ such that for all positive integers $a < p$, if $a$ is a quadratic residue of $p$, then every divisor of $a$ is still a quadratic residue of $p$.

import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Data.ZMod.Defs

def answer : Set ℕ := sorry

theorem solution : { p : ℕ | p.Prime ∧ ∀ a, 0 < a → a < p → IsSquare (a : ZMod p) →
  ∀ b, b ∣ a → IsSquare (b : ZMod p) } = answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions