SmallKernelCharacters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The three nonprincipal kernels of absolute value at most two

theorem OAI.Ostmann.negative_one_kernel_ne_one line 9
theorem OAI.Ostmann.even_one_kernel_ne_one line 19
theorem OAI.Ostmann.exists_negative_one_kernel_character line 35
Source documentation
The small characters are constructed from the same twists and checked at 3 or 5. Their conductors are bounded by the original levels 4 and 8.
```
theorem exists_negative_one_kernel_character :
    ∃ χ : PrimitiveRealCharacter, χ.modulus ≤ 4 ∧
      ∀ p : ℕ, p.Prime → p ≠ 2 → χ.character p = (jacobiSym (-1) p : ℝ) := by
…
```
Mentions: OAI.Ostmann.PrimitiveRealCharacter
theorem OAI.Ostmann.exists_even_one_kernel_character line 53

theorem OAI.Ostmann.exists_nonprincipal_kernel_character line 74

Source documentation

Every nonprincipal nonzero squarefree kernel has the same conductor and odd-prime properties, including the three small cases.

theorem exists_nonprincipal_kernel_character (d : ℤ)
    (hsf : Squarefree d.natAbs) (hzero : d ≠ 0) (hone : d ≠ 1) :
    ∃ (χ : PrimitiveRealCharacter) (N : ℕ),
      0 < N ∧ N ∣ χ.modulus ∧ χ.modulus ≤ 8 * N ∧
      (d.natAbs = N ∨ d.natAbs = 2 * N) ∧
      χ.modulus ≤ 4 * d.natAbs ∧ d.natAbs ≤ 2 * χ.modulus ∧
      ∀ p : ℕ, p.Prime → p ≠ 2 → χ.character p = (jacobiSym d p : ℝ) := by
…

Mentions: OAI.Ostmann.PrimitiveRealCharacter