OAI/Algebra/FiniteTensor/TensorApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Algebraic tensor approximation and the characteristic-zero finite tensor obstruction.

  1. theorem OAI.PD4Tensor.Spreading.tensor_algebraic_approximation line 20
  2. theorem OAI.PD4Tensor.Spreading.tensor_algebraic_approximation_target line 52
  3. theorem OAI.PD4Tensor.Spreading.no_formal_tensor_model line 58
  4. def OAI.PD4Tensor.Spreading.sourceIndex line 99
  5. def OAI.PD4Tensor.Spreading.sourceModel line 107
  6. theorem OAI.PD4Tensor.Spreading.source_primitives_exist line 129
  7. theorem OAI.required_finite_tensor_obstruction line 139