OAI/Algebra/FormulaHitting/WordIndependence.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.NCHitting.PolyWords line 15
  2. def OAI.NCHitting.polynomialEncode line 17
  3. theorem OAI.NCHitting.polynomialEncode_single line 24
  4. def OAI.NCHitting.stripLetter line 28
  5. theorem OAI.NCHitting.stripLetter_apply line 32
  6. theorem OAI.NCHitting.stripLetter_single_nil line 36
  7. theorem OAI.NCHitting.stripLetter_single_cons line 42
  8. def OAI.NCHitting.polynomialDifferential line 53
  9. def OAI.NCHitting.polynomialMul line 58
  10. def OAI.NCHitting.polynomialTransform line 63
  11. theorem OAI.NCHitting.polynomialTransform_apply line 68
  12. theorem OAI.NCHitting.polynomialTransform_single_nil line 77
  13. theorem OAI.NCHitting.polynomialTransform_single_cons line 85
  14. theorem OAI.NCHitting.polynomialEncode_transform line 94
  15. def OAI.NCHitting.naturalPoles line 129
  16. theorem OAI.NCHitting.naturalPoles_injective line 131
  17. theorem OAI.NCHitting.natural_poleProduct_ne_zero line 139
  18. theorem OAI.NCHitting.natural_poleProduct_mul_kernel line 144
  19. theorem OAI.NCHitting.natural_poleProduct_derivative line 156
  20. def OAI.NCHitting.LengthBound line 163
  21. def OAI.NCHitting.topSupport line 166
  22. theorem OAI.NCHitting.mem_topSupport line 170
  23. theorem OAI.NCHitting.transform_lengthBound line 175
  24. theorem OAI.NCHitting.transform_top_coefficient line 192
  25. theorem OAI.NCHitting.topSupport_transform_ssubset line 204
  26. theorem OAI.NCHitting.polynomialEncode_eq_zero line 227
  27. theorem OAI.NCHitting.linearCombination_eq_polynomialEncode line 320
  28. theorem OAI.NCHitting.wordSeries_polynomial_independent line 325
  29. theorem OAI.NCHitting.wordSeries_independent line 334