OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeTriangularCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual hyperbolic coordinates of the triangularized cubed-prime branches; the horizontal translation is retained exactly.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix_mobius line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedScale_square line 38
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedScale_translation line 53