OAI/NumberTheory/Ostmann/Preliminaries/SeparatedSetSquares.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The inverse-square row sum for a finite separated set

  1. theorem OAI.Ostmann.positive_set_inverse_squares line 11
  2. theorem OAI.Ostmann.separated_set_inverse_squares line 30