OAI/Algebra/FiniteTensor/FiniteObstruction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite chart obstruction and formal evaluation of separated potentials.

  1. def OAI.PD4Tensor.TruncatedForms.sigmaDeformed line 23
  2. theorem OAI.PD4Tensor.TruncatedForms.finite_chart_obstruction line 31
  3. theorem OAI.PD4Tensor.FrobeniusTruncation.formalEval_rename line 111
  4. theorem OAI.PD4Tensor.FiniteCoordinates.nilEval_extension line 128
  5. theorem OAI.PD4Tensor.TruncatedForms.formalSigmaPotential_eval line 157
  6. theorem OAI.PD4Tensor.TruncatedForms.formalSigmaSelected_eval line 163
  7. theorem OAI.PD4Tensor.TruncatedForms.formalSigmaDeformed_eval line 170
  8. theorem OAI.PD4Tensor.nilEval_zero line 201