Symmetry lemmas relating to units

Symmetry properties

theorem complexLorentzTensor.coContrUnit_symm : coContrUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) contrCoUnit

Swapping indices of coContrUnit returns contrCoUnit: {δ' | μ ν = δ | ν μ}ᵀ.

theorem complexLorentzTensor.contrCoUnit_symm : contrCoUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) coContrUnit

Swapping indices of contrCoUnit returns coContrUnit: {δ | μ ν = δ' | ν μ}ᵀ.

theorem complexLorentzTensor.altLeftLeftUnit_symm : altLeftLeftUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) leftAltLeftUnit

Swapping indices of altLeftLeftUnit returns leftAltLeftUnit: {δL' | α α' = δL | α' α}ᵀ.

theorem complexLorentzTensor.leftAltLeftUnit_symm : leftAltLeftUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) altLeftLeftUnit

Swapping indices of leftAltLeftUnit returns altLeftLeftUnit: {δL | α α' = δL' | α' α}ᵀ.

theorem complexLorentzTensor.altRightRightUnit_symm : altRightRightUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) rightAltRightUnit

Swapping indices of altRightRightUnit returns rightAltRightUnit: {δR' | β β' = δR | β' β}ᵀ.

theorem complexLorentzTensor.rightAltRightUnit_symm : rightAltRightUnit = (TensorSpecies.Tensor.permT ![1, 0] ⋯) altRightRightUnit

Swapping indices of rightAltRightUnit returns altRightRightUnit: {δR | β β' = δR' | β' β}ᵀ.