OAI/NumberTheory/Ostmann/Quadratic/QuadraticRestrictedBilinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Divisor restrictions shorten each side of the coprime bilinear form

The Möbius divisor is kept separate from the fixed divisor. No replacement of two divisibility conditions by their product is needed.

  1. theorem OAI.Ostmann.quadratic_restricted_transpose_energy line 15
  2. theorem OAI.Ostmann.quadratic_coprime_restricted_bound line 41