OAI/NumberTheory/CubicMoment/Estimates/CubicNumeratorCubeFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Multiplication by a nonzero cube changes only deleted Euler factors, not principality of the cubic numerator character.

  1. lemma OAI.CubicFirstMoment.cubicNumeratorChar_mul_cube_ne_one line 10
  2. lemma OAI.CubicFirstMoment.cubicNumeratorChar_mul_cube_ne_one_iff line 31