Project-declaredLean 4.32.0
Prod eq sum eval
TensorSpecies.Tensorial.prod_eq_sum_eval
Plain-language statement
Double basis expansion of an element of a tensor product M ⊗[k] M₂ of two Tensorial one-index spaces. Given bases b, b2 of M, M₂ coming from the single-index tensor bases, every x : M ⊗[k] M₂ is the double sum over i, j of the iterated evaluation coefficient toField (evalT 0 j (evalT 0 i (toTensor x))) times b i ⊗ₜ b2 j.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.