OAI/NumberTheory/CubicMoment/Angular/AngularStoppedRoughDivisorMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete divisor mass differs from its empty row by the two controlled tails. The roughness premise concerns the actual coefficients.

  1. theorem OAI.CubicFirstMoment.angular_stopped_rough_divisor_mass line 21