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

docs: field to comm ring

Browse source
This commit is contained in:
jstoobysmith 2024-11-04 13:45:46 +00:00
parent 718583ff49
commit 297557bbb8
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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