OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionDifferential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transport actual horizontal derivatives through the inversion law. This is a chain-rule lemma; all its regularity hypotheses are subsequently supplied by the convergent theta expansion.

  1. theorem OAI.CubicFirstMoment.cubicTheta_inversion_horizontal_deriv line 12