OAI/NumberTheory/Ostmann/QuadraticCenter/SquarefreeFrequency.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The unique squarefree frequency decomposition

  1. theorem OAI.Ostmann.squarefree_square_decomposition_unique line 11
  2. structure OAI.Ostmann.SquarefreeFrequency line 31

    Source documentation

    The squarefree kernel is divided into the part supported on L and the part coprime to L. Positivity excludes the zero frequency.

    structure SquarefreeFrequency (L u : ℕ) where
…
  3. theorem OAI.Ostmann.exists_squarefreeFrequency line 43
  4. theorem OAI.Ostmann.SquarefreeFrequency.v_eq_gcd line 63
  5. theorem OAI.Ostmann.SquarefreeFrequency.unique line 67
  6. theorem OAI.Ostmann.SquarefreeFrequency.s_squarefree line 78
  7. theorem OAI.Ostmann.SquarefreeFrequency.v_squarefree line 81
  8. theorem OAI.Ostmann.SquarefreeFrequency.s_le line 84
  9. theorem OAI.Ostmann.SquarefreeFrequency.w_sq_le line 90