OAI/NumberTheory/CubicMoment/Estimates/ResidueProducts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Products of the actual finite residue characters, including overlapping moduli. The ideal coefficients are exactly the products of the two factors.

  1. def OAI.CubicFirstMoment.residueProductLift line 10
  2. lemma OAI.CubicFirstMoment.residueProductLift_congr line 14
  3. lemma OAI.CubicFirstMoment.residueProductLift_mul line 23
  4. lemma OAI.CubicFirstMoment.residueProductLift_nonunit line 29
  5. def OAI.CubicFirstMoment.productResidueChar line 40
  6. lemma OAI.CubicFirstMoment.productResidueChar_mk line 57
  7. lemma OAI.CubicFirstMoment.productResidueChar_units line 63
  8. lemma OAI.CubicFirstMoment.residueIdealChar_product line 70
  9. lemma OAI.CubicFirstMoment.productResidueChar_induces line 75