OAI/NumberTheory/Ostmann/QuadraticSieve/SquarefreeJacobiCharacter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The conductor of the Jacobi character at odd squarefree level

  1. theorem OAI.Ostmann.jacobi_crt_negative line 11
  2. theorem OAI.Ostmann.jacobiCharacter_squarefree_primitive line 44

    Source documentation

    An odd prime factor missing from the conductor is contradicted by a CRT unit whose Jacobi value is -1 and whose conductor residue is 1.

    theorem jacobiCharacter_squarefree_primitive (N : ℕ) [NeZero N]
    (hN : Squarefree N) (hodd : Odd N) : (jacobiCharacter N).IsPrimitive := by
…

    Mentions: OAI.Ostmann.jacobiCharacter