OAI/NumberTheory/Ostmann/Characters/CycleMellin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Mellin constraint retained by cycle averaging

Reciprocal multiplication retains exactly the character tuples whose signed product is principal. This is the relation used in the final cycle-coefficient estimate.

  1. theorem OAI.Ostmann.mulChar_product_apply line 25
  2. theorem OAI.Ostmann.cycleAverage_product_mellin line 34