OAI/NumberTheory/Ostmann/Arithmetic/PrimePowerSquares.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_power_square_fiber_card_le line 11
2. theorem OAI.Ostmann.distinct_primes_square_budget line 19
3. theorem OAI.Ostmann.prime_powers_square_fiber_card_le line 48

   Source documentation

   For a modulus presented as a product of distinct prime powers, every unit square has at most 2^(number of primes + 1) roots.

   theorem prime_powers_square_fiber_card_le {I : Type*} [Fintype I]
       (p n : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i ^ n i)]
       [NeZero (∏ i, p i ^ n i)] (hp : Function.Injective p)
       (hc : Pairwise (fun i j => (p i ^ n i).Coprime (p j ^ n j)))
       (a : (ZMod (∏ i, p i ^ n i))ˣ) :
       Nat.card {x : (ZMod (∏ i, p i ^ n i))ˣ // x ^ 2 = a} ≤
         2 ^ (Fintype.card I + 1) := by
   …