Symmetry lemmas relating to units

Symmetry properties

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

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

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

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

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

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

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

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

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

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

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

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