OAI/NumberTheory/CubicMoment/Estimates/PrimaryProductCoefficients.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of ideal convolution coefficients with the finite fibres of products of primary Eisenstein elements.

  1. lemma OAI.CubicFirstMoment.idealExponentOf_primary_prod line 12
  2. lemma OAI.CubicFirstMoment.primary_eq_of_idealExponentOf_eq line 26
  3. theorem OAI.CubicFirstMoment.coeff_product_primary_fiber line 32