OAI/NumberTheory/CubicMoment/Decomposition/StoppedRoughDivisorMass.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.stopped_rough_divisor_mass line 15