From 721c6bffb618a89adc685d01b79a1ee4f6331ce1 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 31 Oct 2024 05:33:39 +0000
Subject: [PATCH] Add .gitpod.yml

---
 .gitpod.yml                                       | 12 ++++++++++++
 HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean |  2 ++
 2 files changed, 14 insertions(+)
 create mode 100644 .gitpod.yml

diff --git a/.gitpod.yml b/.gitpod.yml
new file mode 100644
index 0000000..7789c01
--- /dev/null
+++ b/.gitpod.yml
@@ -0,0 +1,12 @@
+# This is run when starting a Gitpod workspace on this repository
+
+image: leanprovercommunity/gitpod4
+
+vscode:
+  extensions:
+    - leanprover.lean4 # install the Lean 4 VS Code extension
+
+tasks:
+  - init: |
+      elan self update
+      lake exe cache get
diff --git a/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
index 37a1e14..a5096ad 100644
--- a/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Metrics/Basis.lean
@@ -52,6 +52,8 @@ lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+/-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as
+a tensor tree.-/
 lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 0))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 1)))) <|