OAI/NumberTheory/CubicMoment/Theta/CubicThetaKubotaCharacter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cubic Kubota character on the actual principal congruence group Gamma_1(3) of DR v3 (5.4). Multiplicativity is derived from reciprocity, including the noncoprime and zero-entry cases.

  1. lemma OAI.CubicFirstMoment.cubicThetaKubotaValue_eq_symbol line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaKubotaValue_mul line 24
  3. def OAI.CubicFirstMoment.cubicThetaKubotaCharacter line 39

    Source documentation

    The published multiplier is a genuine multiplicative character.

    def cubicThetaKubotaCharacter : cubicThetaPrincipalGroup →* ℂ where
…

    Mentions: OAI.CubicFirstMoment.cubicThetaPrincipalGroup

  4. lemma OAI.CubicFirstMoment.cubicThetaKubotaCharacter_cube line 44