From 1aeda9c713e80f6779735b899d9e047c467a6968 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 22 Oct 2024 18:05:38 +0000
Subject: [PATCH] refactor: Lint

---
 HepLean/Tensors/Tree/Elab.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index c34dbfe..561ded5 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -371,8 +371,8 @@ def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ))
 
 /-- Takes two maps `Fin n → Fin n` and returns the equivelance they form. -/
 def finMapToEquiv (f1 : Fin n → Fin m) (f2 : Fin m → Fin n)
-  (h : ∀ x, f1 (f2 x) = x := by decide)
-  (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where
+    (h : ∀ x, f1 (f2 x) = x := by decide)
+    (h' : ∀ x, f2 (f1 x) = x := by decide) : Fin n ≃ Fin m where
   toFun := f1
   invFun := f2
   left_inv := h'
@@ -417,6 +417,7 @@ partial def getIndicesFull (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)
 
 namespace SMul
 
+/-- The syntax associated with the scalar multiplication of tensors. -/
 def smulSyntax (c T : Term) : Term :=
   Syntax.mkApp (mkIdent ``TensorTree.smul) #[c, T]