OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Canonical removal of the free primary cube. The remaining cube part is supported on the level, and the removed factor is coprime to it.

  1. lemma OAI.CubicFirstMoment.cubicTheta_primarySmallPart_supported line 13
  2. def OAI.CubicFirstMoment.CubicThetaCoordinates.coreNumerator line 36
  3. def OAI.CubicFirstMoment.CubicThetaCoordinates.core line 40
  4. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.core_decomposition line 51
  5. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.core_cube_supported line 58
  6. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.free_cube_coprime line 63
  7. theorem OAI.CubicFirstMoment.CubicThetaCoordinates.common_coefficient_core line 68
  8. theorem OAI.CubicFirstMoment.CubicThetaCoordinates.common_tau_core line 77