OAI/NumberTheory/Ostmann/Quadratic/QuadraticReciprocityCharacter.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Reciprocity formulas for the sign and two-part of a kernel

  1. theorem OAI.Ostmann.jacobi_odd_numerator_formula line 9
  2. theorem OAI.Ostmann.jacobi_negative_odd_formula line 17
  3. theorem OAI.Ostmann.jacobi_twice_odd_formula line 22
  4. theorem OAI.Ostmann.jacobi_negative_twice_odd_formula line 28
  5. def OAI.Ostmann.realFourCharacter line 34
  6. def OAI.Ostmann.realEightCharacter line 37
  7. theorem OAI.Ostmann.realFourCharacter_apply line 40
  8. theorem OAI.Ostmann.realEightCharacter_apply line 43
  9. def OAI.Ostmann.signedOddKernelCharacter line 47

    Source documentation

    The odd-part character, with the parity twist prescribed by reciprocity.

    noncomputable def signedOddKernelCharacter (N : ℕ) [NeZero N] (negative : Bool) :
    DirichletCharacter ℝ (Nat.lcm N 4) :=
…
  10. theorem OAI.Ostmann.signedOddKernelCharacter_value line 52
  11. def OAI.Ostmann.evenKernelTwist line 75

    Source documentation

    The conductor-eight twist accounts for both the sign and the factor two.

    noncomputable def evenKernelTwist (k : ℕ) : DirichletCharacter ℝ 8 :=
…
  12. theorem OAI.Ostmann.evenKernelTwist_value line 78
  13. def OAI.Ostmann.signedEvenKernelCharacter line 88
  14. theorem OAI.Ostmann.signedEvenKernelCharacter_value line 93