OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootCoverDegree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The root cover has its exact finite subgroup index as measure degree.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootCoverProjection line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootCoverProjection_apply line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootCoverProjection_continuous line 24
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootCoverProjection_measure line 29