OAI/NumberTheory/CubicMoment/Angular/AngularSmallTwistSmoothMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The original primary mixed smooth sum has the cubic second moment. Its primitive characters, conductors, and Euler corrections are constructed.

  1. def OAI.CubicFirstMoment.primaryAngularSmallTwistSmoothSum line 16
  2. theorem OAI.CubicFirstMoment.primary_angular_smalltwist_smooth_cubic_moment line 20