OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeTraceLinear.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Linearity of the literal finite trace, retaining its actual finite-energy section before passing to the completion.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_add line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_smul line 24
  3. def OAI.CubicFirstMoment.cubicThetaPrimeTraceFiniteLinear line 35