Merge pull request #375 from HEPLean/JTS/Docs

refactor: Major refactor of Elab for tensors
HEPLean · Mar 5, 2025 · acd549e · acd549e
2 parents db803e9 + 215a54c
commit acd549e
Show file tree

Hide file tree

Showing 3 changed files with 218 additions and 315 deletions.
diff --git a/PhysLean/Relativity/Tensors/TensorSpecies/Basic.lean b/PhysLean/Relativity/Tensors/TensorSpecies/Basic.lean
@@ -338,6 +338,10 @@ def liftTensor {n : ℕ} {c : Fin n → S.C} {E : Type} [AddCommMonoid E] [Modul
     (S.F.obj (OverColor.mk c) →ₗ[S.k] E) :=
   PiTensorProduct.lift
 
+/-- The number of indices `n` from a tensor. -/
+@[nolint unusedArguments]
+def numIndices {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (_ : S.F.obj (OverColor.mk c)) : ℕ := n
+
 end TensorSpecies
 
 end