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

doc: Update doc for tensor.

Browse source
This commit is contained in:
jstoobysmith 2024-10-31 14:13:35 +00:00
parent aae24f3df7
commit d5fe9c0db6
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -672,8 +672,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
noncomputable section
/-- The underlying tensor a tensor tree corresponds to.
Note: This function is not fully defined yet. -/
/-- The underlying tensor a tensor tree corresponds to. -/
def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (OverColor.mk c) := fun
| tensorNode t => t
| add t1 t2 => t1.tensor + t2.tensor