OAI/NumberTheory/Ostmann/Quadratic/QuadraticSignedFrequencyBijection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Unique signed squarefree coordinates, with exact finite reindexing

  1. theorem OAI.Ostmann.signed_frequency_abs line 11
  2. theorem OAI.Ostmann.signed_odd_kernel_squarefree line 16
  3. theorem OAI.Ostmann.quadratic_signed_coordinates_injective line 25
  4. theorem OAI.Ostmann.quadratic_frequency_coordinates_injOn line 53
  5. theorem OAI.Ostmann.quadratic_frequency_sum_exact line 69