Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersrealLorentzTensor.leviCivita_basis_repr_eq_zero_of_eq
Plain-language statement
The Levi-Civita tensor vanishes on any multi-index with a repeated value: if two distinct index positions i ≠ j carry the same basis index, the component is zero.
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.permT_toComplex
Plain-language statement
The map toComplex commutes with permT.
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.prodT_toComplex
Plain-language statement
The map toComplex commutes with prodT.
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.toComplex_contrP_basisVector
Plain-language statement
For a real basis vector, toComplex(contrP(basisVector c b)) equals contrP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.toComplex_evalP_basisVector
Plain-language statement
For a real basis vector, toComplex(evalP(basisVector c b)) equals evalP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).
Source project: Physlib
Person-level attribution pending.
realLorentzTensor.toComplex_repr
Plain-language statement
The representation of toComplex v in the complexified basis equals the real representation coerced to complex.
Source project: Physlib
Person-level attribution pending.