OAI/NumberTheory/PiExponent/Polynomials/PolynomialFrame.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponentApprox.FramePolynomial line 12
  2. def OAI.PiExponentApprox.logarithmicDerivation line 14
  3. def OAI.PiExponentApprox.polynomialFrame line 20
  4. theorem OAI.PiExponentApprox.derivation_finset_sum_apply line 24
  5. theorem OAI.PiExponentApprox.logarithmicDerivation_apply line 33
  6. theorem OAI.PiExponentApprox.polynomialFrame_zero line 40
  7. theorem OAI.PiExponentApprox.polynomialFrame_pos line 44
  8. theorem OAI.PiExponentApprox.polynomial_pderiv_commute line 48
  9. theorem OAI.PiExponentApprox.pderiv_logarithmicDerivation_commute line 64
  10. theorem OAI.PiExponentApprox.polynomialFrame_commute line 84
  11. theorem OAI.PiExponentApprox.polynomialFrame_add line 102
  12. theorem OAI.PiExponentApprox.polynomialFrame_mul line 107
  13. theorem OAI.PiExponentApprox.polynomialFrame_C line 115
  14. theorem OAI.PiExponentApprox.HasWeightedDegreeLE.logarithmicDerivation line 120
  15. theorem OAI.PiExponentApprox.HasWeightedDegreeLE.polynomialFrame line 129
  16. def OAI.PiExponentApprox.polynomialFrameWord line 140
  17. theorem OAI.PiExponentApprox.polynomialFrameWord_nil line 144
  18. theorem OAI.PiExponentApprox.polynomialFrameWord_cons line 147
  19. theorem OAI.PiExponentApprox.polynomialFrame_commute_word line 152
  20. theorem OAI.PiExponentApprox.HasWeightedDegreeLE.polynomialFrameWord line 162