OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaValue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual principal congruence group and pointwise cubic Kubota multiplier of DR v3 (5.4). Multiplicativity and theta automorphy are not assumed by these arithmetic definitions.

  1. def OAI.CubicFirstMoment.cubicThetaPrincipalGroup line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPrincipalGroup_diagonal_primary line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaPrincipalGroup_column_coprime line 32
  4. def OAI.CubicFirstMoment.cubicThetaKubotaValue line 40

    Source documentation

    The cubic residue value in the original Kubota convention.

    def cubicThetaKubotaValue (g : cubicThetaPrincipalGroup) : ℂ :=
…

    Mentions: OAI.CubicFirstMoment.cubicThetaPrincipalGroup

  5. lemma OAI.CubicFirstMoment.cubicThetaKubotaValue_norm line 43