OAI/NumberTheory/Ostmann/Quadratic/QuadraticKernelConductor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.conductor_dvd_conductor_mul line 11

   Source documentation

   A twist whose conductor is coprime to that of a character cannot remove any of the latter's conductor.

   theorem conductor_dvd_conductor_mul {n : ℕ} [NeZero n]
       (χ ψ : DirichletCharacter ℝ n) (hcop : χ.conductor.Coprime ψ.conductor) :
       χ.conductor ∣ (χ * ψ).conductor := by
   …

2. theorem OAI.Ostmann.odd_part_dvd_twisted_conductor line 20

   Source documentation

   Only the two-part can change when the odd squarefree Jacobi character is multiplied by a character of level coprime to that odd part.

   theorem odd_part_dvd_twisted_conductor (N t : ℕ) [NeZero N] [NeZero t]
       (hN : Squarefree N) (hodd : Odd N) (hcop : N.Coprime t)
       (ψ : DirichletCharacter ℝ t) :
       N ∣ (DirichletCharacter.mul (jacobiCharacter N) ψ).conductor := by
   …

   Mentions: OAI.Ostmann.jacobiCharacter

3. theorem OAI.Ostmann.signedOddKernelCharacter_conductor_bounds line 39
4. theorem OAI.Ostmann.signedEvenKernelCharacter_conductor_bounds line 50