OAI/NumberTheory/CubicMoment/Theta/CubicThetaRationalCusp.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A literal determinant-one lift of each coprime additive numerator. The lift keeps its prescribed bottom-left entry, including ramified factors.

  1. def OAI.CubicFirstMoment.cubicThetaPrimitiveMatrix line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveMatrix_top line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveMatrix_bottom line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveMatrix_cusp line 26
  5. def OAI.CubicFirstMoment.cubicThetaGaussCuspMatrix line 30

    Source documentation

    Lambda cubed cancels the selected frequency denominator.

    def cubicThetaGaussCuspMatrix (r : Eisenstein) (hr : primary r)
    (u : Eisenstein) (hu : IsCoprime r u) : SL(2,Eisenstein) :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary

  6. lemma OAI.CubicFirstMoment.cubicThetaGaussCuspMatrix_bottom line 34
  7. lemma OAI.CubicFirstMoment.cubicThetaGaussCuspMatrix_cusp line 38