OAI/NumberTheory/Ostmann/Arithmetic/SquareCongruence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.squareFiberEquivOne line 12
2. theorem OAI.Ostmann.cyclic_square_fiber_card_le line 19
3. theorem OAI.Ostmann.odd_prime_power_square_fiber_card_le line 33

   Source documentation

   The odd-prime-power part of the manuscript's square-root bound follows from Mathlib's proved cyclicity of the unit group.

   theorem odd_prime_power_square_fiber_card_le (p n : ℕ) [Fact p.Prime]
       (hp2 : p ≠ 2) (a : (ZMod (p ^ n))ˣ) :
       Nat.card {x : (ZMod (p ^ n))ˣ // x ^ 2 = a} ≤ 2 := by
   …

4. def OAI.Ostmann.crtSquareFiberEquiv line 41
5. theorem OAI.Ostmann.crt_square_fiber_card line 58
6. theorem OAI.Ostmann.odd_prime_powers_square_fiber_card_le line 67

   Source documentation

   Exact CRT factorization gives the full odd-prime-power square bound.

   theorem odd_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)]
       (hp2 : ∀ i, p i ≠ 2)
       (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 := by
   …