OAI/NumberTheory/CubicMoment/Angular/AngularTwistedPrimitiveFamily.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 and the exact angular unit condition.

  1. def OAI.CubicFirstMoment.PrimitiveAngularSmallTwistSpecification line 11
  2. theorem OAI.CubicFirstMoment.actual_primitive_angular_smalltwist_family line 19