OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalPeriodMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal bottom-branch periodization has its exact degree as mean.

  1. theorem OAI.CubicFirstMoment.cubicThetaHorizontalPeriodization_mean line 10