OAI/NumberTheory/Ostmann/Arithmetic/MovingNodeCoefficientSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integer substitution on the nonzero original coefficient support

  1. theorem OAI.Ostmann.movingPrimeNodeFactor_substitution_on_right line 9
  2. theorem OAI.Ostmann.movingTemplateCoefficient_integer_node_on_coefficients line 44
  3. theorem OAI.Ostmann.movingTemplateCoefficient_transformed_integer_node_on_coefficients line 140
  4. theorem OAI.Ostmann.movingTemplateCoefficient_averaged_integer_node_on_coefficients line 209
  5. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_next_on_coefficients line 298