OAI/NumberTheory/Ostmann/Preliminaries/CosecantRowSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp row budget for the cosecant matrix

  1. theorem OAI.Ostmann.cosecant_row_sum_bound line 11