OAI/NumberTheory/Ostmann/QuadraticSieve/ComplexJacobiPrimitive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Primitivity of the concrete complex Jacobi character

  1. theorem OAI.Ostmann.real_character_primitive_complex line 12

    Source documentation

    Passing from a real character to its complex values cannot decrease its conductor: the map on values is injective.

    theorem real_character_primitive_complex {N : ℕ} [NeZero N]
    (χ : DirichletCharacter ℝ N) (hχ : χ.IsPrimitive) :
    DirichletCharacter.IsPrimitive (χ.ringHomComp Complex.ofRealHom) := by
…
  2. theorem OAI.Ostmann.jacobiComplex_eq_real_comp line 30
  3. theorem OAI.Ostmann.jacobiComplex_squarefree_primitive line 37
  4. theorem OAI.Ostmann.jacobiComplex_intCast line 42