OAI/Algebra/FiniteTensor/CoefficientDescent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact coefficient descent of formal tensor models.

  1. structure OAI.PD4Tensor.Spreading.CoefficientsIn line 19
  2. theorem OAI.PD4Tensor.Spreading.injective_map_series line 29
  3. def OAI.PD4Tensor.Spreading.descendTensorModel line 39
  4. def OAI.PD4Tensor.Spreading.seriesOver line 121
  5. theorem OAI.PD4Tensor.Spreading.mem_seriesOver line 124
  6. theorem OAI.PD4Tensor.Spreading.coefficients_of_product line 136