refactor(Tensors): rename Tensor.toField to Tensor.toScalar - #1677
Conversation
Rename the map from rank-zero tensors to the scalars `k`, `Tensor.toField`, to
`Tensor.toScalar`, together with its lemmas (`toScalar_default`,
`toScalar_injective`, `toScalar_pure`, `toScalar_permT`, `toScalar_basis_default`,
`toScalar_basis`, `toScalar_eq_repr`, `toScalar_equivariant`, `eq_smul_toScalar`,
`contrT_toScalar`, `Vector.toScalar_eval_eval_eq_tensorProduct_repr`,
`toScalar_conjScalar`). The old name was easily confused with fields in the
electromagnetism files, e.g. `toField {A.toFieldStrength x | [μ] [ν]}ᵀ`.
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
jstoobysmith
left a comment
There was a problem hiding this comment.
Approved - makes sense and looks good
Tensor.toFieldmaps a rank-zero tensor to its underlying scalar ink. In the electromagnetism files it sits right next totoFieldStrength, for exampletoField {A.toFieldStrength x | [μ] [ν]}ᵀ, where "field" reads as a physical field.kis also only assumed to be aCommRing, not a field. This PR renames the map and its lemmas; no statements or proofs change.Renamed (old
toField→ newtoScalar)Relativity/Tensors/Basic.lean:toScalar(def),toScalar_default,toScalar_injective,toScalar_pure,toScalar_permT,toScalar_basis_default,toScalar_basis,toScalar_eq_repr,toScalar_equivariant,eq_smul_toScalarRelativity/Tensors/RealTensor/Basic.lean:contrT_toScalarRelativity/Tensors/RealTensor/Vector/Tensorial.lean:Vector.toScalar_eval_eval_eq_tensorProduct_reprParticles/SuperSymmetry/N1/Basic.lean:toScalar_conjScalarNo deprecated aliases are added.
Reviewer map
Tensors/Basic.lean: the definition and its core lemmas. Docstrings and the section heading now say "scalars" instead of "field".API-map.yaml.🤖 Generated with Claude Code