OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedCoordinateReindex.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact free-coordinate expansion of the distinguished largest-prime role. The global largest prime is retained, including the selected divisor.

  1. lemma OAI.CubicFirstMoment.primeTuple_update_weight line 13
  2. theorem OAI.CubicFirstMoment.distinguished_tuple_largest_reindex line 23