OAI/Algebra/FiniteTensor/RelativeDerivatives.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Relative derivations, graph evaluation and top exterior coefficients.

  1. theorem OAI.PD4Tensor.FiniteCoordinates.pderiv_mem_uniform line 16
  2. def OAI.PD4Tensor.FiniteCoordinates.relativeDeriv line 32
  3. theorem OAI.PD4Tensor.FiniteCoordinates.partial_mk line 40
  4. theorem OAI.PD4Tensor.FiniteCoordinates.partial_coord line 44
  5. theorem OAI.PD4Tensor.FiniteCoordinates.partial_scalar line 51
  6. theorem OAI.PD4Tensor.FiniteCoordinates.partial_mul line 56
  7. theorem OAI.PD4Tensor.FiniteCoordinates.pderiv_commute line 63
  8. theorem OAI.PD4Tensor.FiniteCoordinates.partial_commute line 76
  9. def OAI.PD4Tensor.FiniteCoordinates.partialDerivation line 81
  10. theorem OAI.PD4Tensor.FiniteCoordinates.partial_nilEval line 90
  11. theorem OAI.PD4Tensor.nilEval_rename line 106
  12. theorem OAI.PD4Tensor.ideal_span_range_map line 115
  13. theorem OAI.PD4Tensor.graph_eval line 128
  14. def OAI.PD4Tensor.Forms.topExterior line 156
  15. theorem OAI.PD4Tensor.Forms.topExterior_ιMulti line 161
  16. def OAI.PD4Tensor.Forms.topCoefficient line 167
  17. theorem OAI.PD4Tensor.Forms.topCoefficient_tmul line 171
  18. def OAI.PD4Tensor.Forms.oneFormLinear line 176
  19. def OAI.PD4Tensor.Forms.exteriorScalarExtension line 187
  20. theorem OAI.PD4Tensor.Forms.exteriorScalarExtension_ι line 190
  21. theorem OAI.PD4Tensor.Forms.exteriorScalarExtension_ιMulti line 194
  22. theorem OAI.PD4Tensor.Forms.topCoefficient_oneForm_product line 203