OAI/NumberTheory/CubicMoment/Estimates/TwistedPrimitiveFamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Choosing the actual primitive characters for a finite family, with uniform arithmetic conductor bounds.

  1. def OAI.CubicFirstMoment.PrimitiveSmallTwistSpecification line 11
  2. theorem OAI.CubicFirstMoment.actual_primitive_smalltwist_family line 19