OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootCoverTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual fractional roots preserve hyperbolic measure on their finite arithmetic cover, by transport of the proved fundamental domain.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootImage_fundamental line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRoot_map_restrict line 27
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootCoverTranslate_measurePreserving line 44