OAI/NumberTheory/CubicMoment/Theta/CubicThetaHermitianMetric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Determinant-one Hermitian coordinates and the invariant two-point quantity underlying the hyperbolic metric.

  1. def OAI.CubicFirstMoment.cubicThetaUnitHermitian line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaUnitHermitian_mobius line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaUnitHermitian_pair_det_invariant line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaUnitHermitian_pair_det line 39
  5. def OAI.CubicFirstMoment.cubicThetaHyperbolicChord line 52
  6. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicChord_invariant line 55