OAI/Algebra/FiniteTensor/JetTopology.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Jet ideals, completion and finite polynomial approximation statements.

  1. abbrev OAI.PD4Tensor.Spreading.jetIdeal line 16
  2. theorem OAI.PD4Tensor.Spreading.map_jetIdeal_completion line 18
  3. theorem OAI.PD4Tensor.Spreading.jetIdeal_power_completion line 28
  4. theorem OAI.PD4Tensor.Spreading.mem_completion_power_iff line 35
  5. theorem OAI.PD4Tensor.Spreading.mem_jetIdeal_pow_iff_coeff line 54
  6. theorem OAI.PD4Tensor.Spreading.mem_jetIdeal_pow_iff_order line 60
  7. theorem OAI.PD4Tensor.Spreading.truncate_close_jetIdeal line 68
  8. theorem OAI.PD4Tensor.Spreading.quotient_jet_control line 80
  9. theorem OAI.PD4Tensor.Spreading.high_order_not_divisibility line 95
  10. theorem OAI.PD4Tensor.Spreading.option_series_polynomial_square line 112
  11. theorem OAI.PD4Tensor.Spreading.option_series_polynomial_square_symm line 124
  12. theorem OAI.PD4Tensor.Spreading.algebraic_option_series_symm line 147
  13. theorem OAI.PD4Tensor.Spreading.algebraic_option_series line 155
  14. theorem OAI.PD4Tensor.Spreading.finite_weierstrass_unit_constraints line 173
  15. theorem OAI.PD4Tensor.Spreading.jetIdeal_eq_maximalIdeal line 221
  16. theorem OAI.PD4Tensor.Spreading.jetIdeal_pow_le_jacobson line 234
  17. theorem OAI.PD4Tensor.Spreading.option_coefficient_jet_map_le line 241
  18. theorem OAI.PD4Tensor.Spreading.option_coefficient_jet_pow_map_le line 253
  19. theorem OAI.PD4Tensor.Spreading.option_inverse_coefficient_jet line 261
  20. def OAI.PD4Tensor.Spreading.PolynomialArtinAt line 277
  21. theorem OAI.PD4Tensor.Spreading.PolynomialArtinAt.finite line 287