OAI/NumberTheory/CubicGauss/Cutoffs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Primary squarefree balls and unique square-cube decompositions.

  1. lemma OAI.CubicFirstMoment.squarefree_mul_of_coprime line 16
  2. lemma OAI.CubicFirstMoment.cubicSymbol_cube line 20
  3. theorem OAI.CubicFirstMoment.cubicSymbol_cube_decomposition line 29
  4. lemma OAI.CubicFirstMoment.norm_lambdaE line 38
  5. lemma OAI.CubicFirstMoment.normNat_lambdaE line 43
  6. lemma OAI.CubicFirstMoment.lambdaE_prime line 46

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/CubicSupplementaryPeriodicityProof.lean:255 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.lambdaE_prime@path.

  7. theorem OAI.CubicFirstMoment.full_cube_decomposition_unit line 67