OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteInflation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact multiplicity in a finite residue-ring inflation. The surjective reduction is used directly, so no choice of residue representatives enters the resulting sum identity.

  1. lemma OAI.CubicFirstMoment.finite_sum_surjective_addHom line 12
  2. theorem OAI.CubicFirstMoment.residue_sum_inflation line 36
  3. lemma OAI.CubicFirstMoment.residueFourierChar_mul_factor line 56
  4. theorem OAI.CubicFirstMoment.residueFourier_inflation line 70
  5. theorem OAI.CubicFirstMoment.residueFourier_inflation_of_eq line 92