Documentation typo in tensor product example refers to undefined `T1` instead

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in Physlib/Relativity/Tensors/Elab.lean (around line 31) is incorrect.

Current text

Suppose `T2` is a tensor with color `![c3]`.
  Then `{T | μ ν ⊗ T2 | σ}ᵀ` is `prodNode (tensorNode T1) (tensorNode T2)`.

Why this is wrong

The documentation example claims that {T | μ ν ⊗ T2 | σ}ᵀ elaborates to prodNode (tensorNode T1) (tensorNode T2). This is incorrect because the preceding sentence introduces T, not T1, as the tensor with color ![c3]. The use of T1 refers to an undefined variable, while T is explicitly mentioned in the context.

The correction replaces T1 with T, aligning the example with the declared tensor name. This matches the structure of other examples in the file, which consistently use T and T2 when discussing tensor products. The error likely arose from a copy-paste mistake or typo during documentation authorship.

The fix ensures consistency with Lean's elaboration logic, as the code in TensorExpressionOperator.prod correctly constructs prodNode from the tensors passed to it. Using T1 would incorrectly imply a separate tensor not mentioned in the example.

Suggested correction

Suppose `T2` is a tensor with color `![c3]`.
  Then `{T | μ ν ⊗ T2 | σ}ᵀ` is `prodNode (tensorNode T) (tensorNode T2)`.

Open Physlib/Relativity/Tensors/Elab.lean around lines 31–32 and review the tensor product example in context. Verify that the introduced tensor is named T, then correct the example so its prodNode reference uses T consistently with T2. Done means the documentation no longer refers to the undefined T1.