OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedTupleRows.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original distinguished-role tuple sum is exactly the sum of the free-prime rows; the global largest-prime and stopping tests are retained.

  1. lemma OAI.CubicFirstMoment.complementTuple_update_product line 15
  2. theorem OAI.CubicFirstMoment.distinguished_tuple_stopped_rows line 23