OAI/NumberTheory/CubicMoment/Theta/CubicThetaAxisLineDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pure coordinate second derivatives are derivatives along the corresponding fixed real tangent direction.

  1. lemma OAI.CubicFirstMoment.cubicThetaAxisFirst_translate line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaAxisFirst_hasLineDerivAt line 18