OAI/NumberTheory/CubicMoment/Theta/CubicThetaBottomRow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual primitive bottom rows for the cubic Eisenstein series. Every admissible row is completed inside the principal level-three group, using Bezout with 3c rather than an unproved choice of congruences.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrincipalGroup_mem_iff line 13
  2. structure OAI.CubicFirstMoment.CubicThetaBottomRow line 44
  3. def OAI.CubicFirstMoment.cubicThetaBottomRow line 51
  4. theorem OAI.CubicFirstMoment.cubicThetaBottomRow_surjective line 60
  5. def OAI.CubicFirstMoment.CubicThetaBottomRow.completion line 78

    Source documentation

    A completion of the bottom row, with its existence proved above.

    def CubicThetaBottomRow.completion (r : CubicThetaBottomRow) : cubicThetaPrincipalGroup :=
…

    Mentions: OAI.CubicFirstMoment.CubicThetaBottomRow, OAI.CubicFirstMoment.cubicThetaPrincipalGroup

  6. lemma OAI.CubicFirstMoment.CubicThetaBottomRow.completion_row line 81