OAI/Algebra/FiniteTensor/ArtinCoefficients.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient equations and exact polynomial remainder reconstruction.

  1. abbrev OAI.PD4Tensor.Spreading.CoefficientVariables line 16
  2. instance OAI.PD4Tensor.Spreading.(instance at line 19) line 19
  3. instance OAI.PD4Tensor.Spreading.(instance at line 23) line 23
  4. def OAI.PD4Tensor.Spreading.coefficientPolynomial line 28
  5. def OAI.PD4Tensor.Spreading.coefficientPoint line 34
  6. def OAI.PD4Tensor.Spreading.realizeCoefficients line 38
  7. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_original line 42
  8. theorem OAI.PD4Tensor.Spreading.map_coefficientPolynomial line 48
  9. def OAI.PD4Tensor.Spreading.coefficientRelation line 63
  10. theorem OAI.PD4Tensor.Spreading.map_coefficientRelation line 68
  11. abbrev OAI.PD4Tensor.Spreading.CoefficientEquations line 89
  12. instance OAI.PD4Tensor.Spreading.(instance at line 92) line 92
  13. instance OAI.PD4Tensor.Spreading.(instance at line 95) line 95
  14. def OAI.PD4Tensor.Spreading.coefficientEquation line 98
  15. theorem OAI.PD4Tensor.Spreading.coefficient_equations_iff line 104
  16. theorem OAI.PD4Tensor.Spreading.coefficient_equations_original line 123
  17. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_degree line 131
  18. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_coeff line 142
  19. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_close line 155
  20. theorem OAI.PD4Tensor.Spreading.algebraic_coefficient_series line 179
  21. theorem OAI.PD4Tensor.Spreading.polynomial_series_algebraic_coefficients line 186
  22. theorem OAI.PD4Tensor.Spreading.polynomial_coefficient_close line 206
  23. theorem OAI.PD4Tensor.Spreading.polynomial_series_close line 215
  24. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_algebraic line 232
  25. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_series_algebraic line 243
  26. theorem OAI.PD4Tensor.Spreading.realizeCoefficients_series_close line 248
  27. theorem OAI.PD4Tensor.Spreading.monic_coefficient_close_ne_zero line 261