OAI/Algebra/FiniteTensor/PolynomialApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Algebraic derivatives, minor induction and polynomial Artin approximation.

  1. theorem OAI.PD4Tensor.Spreading.aeval_isAlgebraic line 15
  2. theorem OAI.PD4Tensor.Spreading.algebraic_series_pderiv line 22
  3. theorem OAI.PD4Tensor.Spreading.algebraic_series_rename line 80
  4. theorem OAI.PD4Tensor.Spreading.aeval_minorPolynomial line 99
  5. theorem OAI.PD4Tensor.Spreading.rename_polynomial_square line 107
  6. theorem OAI.PD4Tensor.Spreading.minor_artin_step line 119
  7. theorem OAI.PD4Tensor.Spreading.polynomial_artin line 197