Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Character.Permutation

The six permuted tensor characters #

Precomposing a character with a leg permutation gives another character. The six resulting values multiply to the symmetrized product, and each singleton leg exponent occurs twice among their first-leg exponents.

source
def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character {K : Type} [Field K] (χ : Character K) :
Character K

The reflected character exchanges the second and third tensor legs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_value {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) :
    χ.swap23Character.value T = χ.value fun (x : X) (z : Z) (y : Y) => T x y z
    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.permutedCharacter {K : Type} [Field K] (χ : Character K) (i : Fin 6) :
    Character K

    The three cyclic orders followed by their reflected orders.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.prod_permutedCharacter_value {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) :
      ∏ i : Fin 6, (χ.permutedCharacter i).value T = χ.sixfoldProduct T

      The six permuted characters give exactly the sixfold product on any legs.

      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pX {K : Type} [Field K] (χ : Character K) :
      χ.cyclicCharacter.pX = χ.pZ
      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pY {K : Type} [Field K] (χ : Character K) :
      χ.cyclicCharacter.pY = χ.pX
      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pZ {K : Type} [Field K] (χ : Character K) :
      χ.cyclicCharacter.pZ = χ.pY
      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pX {K : Type} [Field K] (χ : Character K) :
      χ.swap23Character.pX = χ.pX
      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pY {K : Type} [Field K] (χ : Character K) :
      χ.swap23Character.pY = χ.pZ
      source
      @[simp]
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pZ {K : Type} [Field K] (χ : Character K) :
      χ.swap23Character.pZ = χ.pY
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.sum_permutedCharacter_pX {K : Type} [Field K] (χ : Character K) :
      ∑ i : Fin 6, (χ.permutedCharacter i).pX = 2 * (χ.pX + χ.pY + χ.pZ)

      Each singleton-leg exponent occurs twice among the first-leg exponents.