OAI/NumberTheory/CubicMoment/Theta/CubicThetaFullLevelRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

All level-three rows before the coprimality restriction. They form one explicit affine lattice; primary common factors preserve the lattice.

  1. structure OAI.CubicFirstMoment.CubicThetaFullRow line 11
  2. def OAI.CubicFirstMoment.cubicThetaFullRowCoordinates line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaFullRowCoordinates_injective line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaFullRowCoordinates_surjective line 32
  5. def OAI.CubicFirstMoment.cubicThetaFullRowEquiv line 43
  6. def OAI.CubicFirstMoment.CubicThetaFullRow.height line 47
  7. def OAI.CubicFirstMoment.cubicThetaFullRowMultiply line 50
  8. lemma OAI.CubicFirstMoment.cubicThetaFullRowMultiply_height line 56