OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointC1Inversion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Global inversion for the actual gradient pairing.

  1. lemma OAI.CubicFirstMoment.cubicThetaPointC1Inversion_covariance line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaPointC1Inversion_gradient_pairing line 21