OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonCoefficient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The common-factor coefficient is an actual shortened stopped row with a fixed cubic numerator. The normalized Gauss factors cancel exactly.

  1. lemma OAI.CubicFirstMoment.common_gramUntwist_eq line 13
  2. lemma OAI.CubicFirstMoment.stopped_residualRows_eq_slice line 29
  3. lemma OAI.CubicFirstMoment.stopped_common_coefficient_eq line 37
  4. lemma OAI.CubicFirstMoment.stopped_common_character_sum line 49
  5. lemma OAI.CubicFirstMoment.coprimeDispersionGram_congr_coefficients line 68
  6. lemma OAI.CubicFirstMoment.coprimeDispersionGram_unit_scalar line 79
  7. lemma OAI.CubicFirstMoment.stopped_common_gram_eq line 97