DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-10-22 18:05:38 +00:00
parent a6cd796df2
commit 1aeda9c713
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean/Tensors/Tree/Elab.lean
View file

@ -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]