OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimitiveAction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The right action of the full integral modular group on primitive rows. This transports the positive scalar cutoff into a fixed Siegel set.

  1. def OAI.CubicFirstMoment.CubicThetaPrimitiveRow.completion line 11
  2. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.completion_row line 14
  3. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.completion_c line 17
  4. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.completion_d line 20
  5. def OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMul line 23
  6. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMul_c line 26
  7. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMul_d line 32
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveRow_mul line 38
  9. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMul_one line 48
  10. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMul_assoc line 51
  11. def OAI.CubicFirstMoment.CubicThetaPrimitiveRow.rightMulEquiv line 56
  12. lemma OAI.CubicFirstMoment.CubicThetaPrimitiveRow.height_rightMul line 67