OAI/NumberTheory/Ostmann/QuadraticSieve/NonsquareJacobiCharacter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete character behind nonsquare Jacobi cancellation

  1. theorem OAI.Ostmann.exists_squarefree_jacobi_level line 11
  2. theorem OAI.Ostmann.exists_nonsquare_jacobi_character line 66

    Source documentation

    At level 8*n the extra nonunit zeroes are exactly the even arguments and the common factors with n. Induction from the nontrivial squarefree kernel preserves nonprincipality.

    theorem exists_nonsquare_jacobi_character (n : ℕ) (hn : 0 < n)
    (hns : ¬IsSquare n) :
    ∃ χ : DirichletCharacter ℝ (8 * n), χ ≠ 1 ∧
      ∀ a : ℕ, χ (a : ZMod (8 * n)) = if Odd a then realJacobi n a else 0 := by
…

    Mentions: OAI.Ostmann.realJacobi