OAI/NumberTheory/Ostmann/QuadraticCenter/ConductorKernelCandidates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finitely many kernel candidates for one exceptional conductor

  1. def OAI.Ostmann.conductorKernelCandidates line 13

    Source documentation

    The eight possible quotients of a conductor by its odd kernel part, with the four possible sign/two factors.

    def conductorKernelCandidates (q : ℕ) : Finset ℤ :=
…
  2. theorem OAI.Ostmann.conductorKernelCandidates_card line 17
  3. theorem OAI.Ostmann.mem_conductorKernelCandidates line 25

    Source documentation

    The divisibility and size facts proved for the constructed characters place the signed kernel on the explicit list for its conductor.

    theorem mem_conductorKernelCandidates (d : ℤ) (q N : ℕ)
    (hN : 0 < N) (hq : 0 < q) (hNq : N ∣ q) (hbound : q ≤ 8 * N)
    (hd : d.natAbs = N ∨ d.natAbs = 2 * N) :
    d ∈ conductorKernelCandidates q := by
…

    Mentions: OAI.Ostmann.conductorKernelCandidates

  4. def OAI.Ostmann.largeConductorKernelCandidates line 50
  5. theorem OAI.Ostmann.largeConductorKernelCandidates_card line 53
  6. theorem OAI.Ostmann.mem_largeConductorKernelCandidates line 57