OAI/Algebra/FiniteTensor/PositiveObstruction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Positive-characteristic tensor obstruction and exact formal parametrization conditions.

  1. theorem OAI.PD4Tensor.TruncatedForms.formal_positive_obstruction line 23
  2. theorem OAI.PD4Tensor.TruncatedForms.formal_active_obstruction line 126
  3. def OAI.PD4Tensor.TruncatedForms.formalAnyPotential line 198
  4. def OAI.PD4Tensor.TruncatedForms.formalAnyDeformed line 202
  5. theorem OAI.PD4Tensor.TruncatedForms.formal_active_obstruction_any line 213
  6. abbrev OAI.PD4Tensor.Coordinates line 258
  7. abbrev OAI.PD4Tensor.N line 260
  8. def OAI.PD4Tensor.includeBlock line 263
  9. structure OAI.PD4Tensor.Germs line 268
  10. def OAI.PD4Tensor.Germs.Sā‚€ line 278
  11. def OAI.PD4Tensor.Germs.B line 282
  12. def OAI.PD4Tensor.Germs.Sā‚œ line 286
  13. structure OAI.PD4Tensor.Parametrizations line 295
  14. def OAI.PD4Tensor.Parametrizations.leftTangent line 304
  15. def OAI.PD4Tensor.Parametrizations.rightTangent line 308
  16. def OAI.PD4Tensor.Germs.leftJacobian line 312
  17. def OAI.PD4Tensor.Germs.rightJacobian line 318
  18. structure OAI.PD4Tensor.TensorConditions line 326
  19. def OAI.PD4Tensor.FiniteTensorObstruction line 339
  20. theorem OAI.PD4Tensor.positiveTensorObstruction line 355