OAI/NumberTheory/CubicMoment/Estimates/MixedPrimitiveFamily.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniformly selecting the primitive character attached to each actual mixed pair in a finite family, with no character-existence hypothesis.

  1. def OAI.CubicFirstMoment.PrimitiveMixedSpecification line 11
  2. theorem OAI.CubicFirstMoment.actual_primitive_mixed_family line 18
  3. lemma OAI.CubicFirstMoment.ramifiedEulerNorm_le line 35