OAI/Algebra/FiniteTensor/DeformedGraphs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Separated potentials, parameter selection and complementary deformed graphs.

  1. def OAI.PD4Tensor.TruncatedForms.formalSigmaPotential line 19
  2. def OAI.PD4Tensor.TruncatedForms.formalSigmaSelected line 24
  3. def OAI.PD4Tensor.TruncatedForms.formalSigmaDeformed line 29
  4. def OAI.PD4Tensor.TruncatedForms.formalActiveDeformed line 47
  5. theorem OAI.PD4Tensor.TruncatedForms.augmentation_formalActiveDeformed line 54
  6. theorem OAI.PD4Tensor.TruncatedForms.sum_threeParameters_activeExtension line 66
  7. theorem OAI.PD4Tensor.TruncatedForms.selector_formalActiveDeformed line 84
  8. theorem OAI.PD4Tensor.TruncatedForms.augmentation_selector_graph line 112
  9. theorem OAI.PD4Tensor.TruncatedForms.central_graph_zero line 122
  10. theorem OAI.PD4Tensor.TruncatedForms.selector_graph_zero line 133
  11. theorem OAI.PD4Tensor.TruncatedForms.selector_graph_triple line 145
  12. theorem OAI.PD4Tensor.TruncatedForms.formalSigmaSelected_active_triple line 179
  13. theorem OAI.PD4Tensor.TruncatedForms.active_right_triples line 192