OfInt

📁 Source: PhysLean/Relativity/Tensors/OfInt.lean

Statistics

Metric	Count
Definitions TensorInt, toTensor	2
Theorems basis_repr_apply, basis_eq_tensorInt	2
Total	4

TensorSpecies.Tensor

Definitions

Name	Category	Theorems
TensorInt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_eq_tensorInt 📖	mathematical	—	ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis TensorInt.toTensor TensorSpecies.repDim	—	TensorInt.basis_repr_apply

TensorSpecies.Tensor.TensorInt

Definitions

Name	Category	Theorems
toTensor 📖	CompOp	2 math math: basis_repr_apply, TensorSpecies.Tensor.basis_eq_tensorInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_repr_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis toTensor	—	—

---

← Back to Index