OAI/NumberTheory/CubicMoment/Theta/CubicThetaMobiusMatrix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Hermitian coordinates for the actual hyperbolic action. They give the composition law without any analytic or automorphy assumption.

  1. def OAI.CubicFirstMoment.cubicThetaHermitian line 11
  2. def OAI.CubicFirstMoment.cubicThetaMobiusQuadratic line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaMobiusQuadratic_entries line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaHermitian_mobius line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaMobiusQuadratic_comp line 55