⚠️ 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/RealTensor/Basic.lean (around line 67) is incorrect.
Current text
/-- The tensor structure for complex Lorentz tensors. -/
Why this is wrong
The docstring for realLorentzTensor incorrectly claims it defines "complex Lorentz tensors", but the declaration's name and surrounding context clearly indicate it is for real tensors. The file's comments explicitly mention "Real Lorentz tensors" and the definition uses Lorentz.ContrMod/Lorentz.CoMod, which are real vector spaces.
This discrepancy arises because the docstring was not updated when the definition was renamed from a complex variant to a real one. The correction aligns the documentation with the actual purpose of realLorentzTensor, which is consistent with the file's focus on real tensor structures and the use of ℝ as the scalar field in its type signature.
Suggested correction
/-- The tensor structure for real Lorentz tensors. -/
Summary
The documentation in
Physlib/Relativity/Tensors/RealTensor/Basic.lean(around line 67) is incorrect.Current text
/-- The tensor structure for complex Lorentz tensors. -/Why this is wrong
The docstring for
realLorentzTensorincorrectly claims it defines "complex Lorentz tensors", but the declaration's name and surrounding context clearly indicate it is for real tensors. The file's comments explicitly mention "Real Lorentz tensors" and the definition usesLorentz.ContrMod/Lorentz.CoMod, which are real vector spaces.This discrepancy arises because the docstring was not updated when the definition was renamed from a complex variant to a real one. The correction aligns the documentation with the actual purpose of
realLorentzTensor, which is consistent with the file's focus on real tensor structures and the use ofℝas the scalar field in its type signature.Suggested correction
/-- The tensor structure for real Lorentz tensors. -/