OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeReductionRow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Primitive rows that triangularize the three nonzero valuation branches of the cubed-prime lower chart.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction_primary line 11
  2. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReductionRow line 19
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction line 30
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction_c line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction_d line 39
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction_determinant line 44
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeReduction_phase line 52