OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspRowTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual primitive bottom rows transported into an arbitrary integral cusp. The row map remains injective and preserves the literal height.

  1. def OAI.CubicFirstMoment.cubicThetaCuspRow line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaCuspRow_coordinates line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaCuspRow_injective line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaCuspRow_height line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaCuspRow_height_zero_c line 53