OAI/Algebra/FiniteTensor/WeierstrassConstraints.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Weierstrass reconstitution and finite constraints for distinguished division.

  1. theorem OAI.PD4Tensor.Spreading.polynomial_eval_divisor_congruence line 16
  2. theorem OAI.PD4Tensor.Spreading.unit_add_jacobson line 31
  3. theorem OAI.PD4Tensor.Spreading.weierstrass_prepared_minor line 41
  4. def OAI.PD4Tensor.Spreading.minorPolynomial line 65
  5. theorem OAI.PD4Tensor.Spreading.eval_minorPolynomial line 69
  6. theorem OAI.PD4Tensor.Spreading.reconstitute_close line 85
  7. theorem OAI.PD4Tensor.Spreading.weierstrass_reconstitution line 98
  8. theorem OAI.PD4Tensor.Spreading.reconstitute_algebraic line 122
  9. abbrev OAI.PD4Tensor.Spreading.RemainderVariables line 141
  10. def OAI.PD4Tensor.Spreading.remainderPoint line 143
  11. def OAI.PD4Tensor.Spreading.remainderEmbedding line 146
  12. def OAI.PD4Tensor.Spreading.remainderEquation line 148
  13. theorem OAI.PD4Tensor.Spreading.eval_remainderEmbedding line 154
  14. theorem OAI.PD4Tensor.Spreading.remainder_equations_iff line 162
  15. theorem OAI.PD4Tensor.Spreading.remainder_point_reconstruct line 192
  16. theorem OAI.PD4Tensor.Spreading.powerSeries_constant_mem line 211
  17. theorem OAI.PD4Tensor.Spreading.powerSeries_map_jacobson line 220
  18. theorem OAI.PD4Tensor.Spreading.powerSeries_unit_close line 229
  19. theorem OAI.PD4Tensor.Spreading.powerSeries_jacobson_close line 241
  20. abbrev OAI.PD4Tensor.Spreading.seriesCoefficientMap line 258
  21. theorem OAI.PD4Tensor.Spreading.eval_seriesCoefficientMap line 262
  22. theorem OAI.PD4Tensor.Spreading.coefficient_prepared_point line 272
  23. theorem OAI.PD4Tensor.Spreading.distinguished_dvd_of_series_dvd line 347
  24. theorem OAI.PD4Tensor.Spreading.eval₂_dvd_sub line 358
  25. theorem OAI.PD4Tensor.Spreading.finite_weierstrass_constraints line 379