From 297557bbb8058c69ce54477d87f98de7e1ad4c76 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 4 Nov 2024 13:45:46 +0000 Subject: [PATCH] docs: field to comm ring --- HepLean/Tensors/Tree/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index f357a09..e38500b 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -40,7 +40,8 @@ open MonoidalCategory /-- The sturcture of a type of tensors e.g. Lorentz tensors, Einstien tensors, complex Lorentz tensors. -/ structure TensorSpecies where - /-- The field over which we want to consider the tensors to live in, usually `ℝ` or `ℂ`. -/ + /-- The commutative ring over which we want to consider the tensors to live in, + usually `ℝ` or `ℂ`. -/ k : Type /-- An instance of `k` as a commutative ring. -/ k_commRing : CommRing k