OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeResidueComplement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The unit and complementary chart parameters exhaust the residue ring modulo p^3 without overlap or multiplicity.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueComplement_sum line 10