OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeTriangular.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact triangularization of the nonzero valuation branches in the cubed-prime trace. The matrices are the actual integral row completions.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedScale line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedScale_ne_zero line 14
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix line 19
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix_c line 25
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix_d line 58
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix_b line 76
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReducedMatrix_a line 94