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

refactor: Update succAbove notation for tensor tree

Browse source
This commit is contained in:
jstoobysmith 2024-11-05 10:46:18 +00:00
parent da6679ea90
commit bfaaf36485
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/Tensors/Tree/Basic.lean
View file

@ -572,10 +572,10 @@ inductive TensorTree (S : TensorSpecies) : {n : ℕ} → (Fin n → S.C) → Typ
/-- A node corresponding to the contraction of indices of a tensor. -/
| contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) →
(j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c →
TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
TensorTree S (c ∘ i.succAbove ∘ j.succAbove)
/-- A node corresponding to the evaluation of an index of a tensor. -/
| eval {n : ℕ} {c : Fin n.succ → S.C} : (i : Fin n.succ) → (x : ℕ) → TensorTree S c →
TensorTree S (c ∘ Fin.succAbove i)
TensorTree S (c ∘ i.succAbove)
namespace TensorTree