OAI/Algebra/FiniteTensor/PreparedApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed-jet approximation of prepared systems and the aligned Artin step.

  1. theorem OAI.PD4Tensor.Spreading.adic_complete_power line 17
  2. theorem OAI.PD4Tensor.Spreading.prepared_algebraic_approximation line 56
  3. theorem OAI.PD4Tensor.Spreading.order_eq_of_close_jet line 109
  4. theorem OAI.PD4Tensor.Spreading.ne_zero_of_close_jet line 121
  5. theorem OAI.PD4Tensor.Spreading.fixed_jet_prepared_approximation line 141
  6. theorem OAI.PD4Tensor.Spreading.minorPolynomial_map line 196
  7. theorem OAI.PD4Tensor.Spreading.aligned_artin_step line 212