OAI/Geometry/SplitTangent/TensorSectionSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensor Section Space.

  1. lemma OAI.SplitTangent.tangentTensorCoordinates_zero line 18
  2. lemma OAI.SplitTangent.tangentTensorCoordinates_add line 24
  3. lemma OAI.SplitTangent.tangentTensorCoordinates_smul line 31
  4. def OAI.SplitTangent.tensorSectionSpace line 38
  5. def OAI.SplitTangent.tensorSectionSpace.toTensor line 70
  6. def OAI.SplitTangent.tensorSectionSpace.contract line 78
  7. def OAI.SplitTangent.symmetricSupportedTensors line 92
  8. theorem OAI.SplitTangent.PointedGenerated.exists_basis_sections line 125