Derivative

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Derivative.lean

Statistics

Metric	Count
Definitions derivative, mapToBasis, «term∂»	3
Theorems derivative_repr	1
Total	4

realLorentzTensor

Definitions

Name	Category	Theorems
derivative 📖	CompOp	1 math math: derivative_repr
mapToBasis 📖	CompOp	—
«term∂» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivative_repr 📖	mathematical	TensorSpecies.Tensor.ComponentIdx Color LorentzGroup lorentzGroupIsGroup realLorentzTensor mapToBasis TensorSpecies.repDim TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis	TensorSpecies.τ derivative TensorSpecies.Tensor.ComponentIdx.prodEquiv repDim_eq_one_plus_dim	—	repDim_eq_one_plus_dim

---

← Back to Index