Details
Key data structure
The components of tensor, for example a 2-tensor $T^\mu_\nu$, the components would contain all specifications of the index.
Need
This is used to manipulate tensors and extract their components. It is also used with basis of tensors.
What needs doing
Requirements
Corresponding file system
Currently these sit in the file system:
https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/Relativity/Tensors
Details
Key data structure
The components of tensor, for example a 2-tensor$T^\mu_\nu$ , the components would contain all specifications of the index.
ComponentIdxNeed
This is used to manipulate tensors and extract their components. It is also used with basis of tensors.
What needs doing
ComponentIdxand results related there to are currently spread throughout theTensorsdirectory. They should be moved into their own file system.Requirements
Corresponding file system
Currently these sit in the file system:
https://github.com/lean-phys-community/PhysLean/tree/master/PhysLean/Relativity/Tensors