Permutation.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character line 24
Source documentation
The reflected character exchanges the second and third tensor legs.
```
def swap23Character : Character where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_value line 54
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.permutedCharacter line 59
Source documentation
The three cyclic orders followed by their reflected orders.
```
def permutedCharacter (i : Fin 6) : Character :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.prod_permutedCharacter_value line 65

Source documentation

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

theorem prod_permutedCharacter_value {X Y Z : Type}
    [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) :
    (∏ i : Fin 6, (χ.permutedCharacter i).value T) = χ.sixfoldProduct T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pX line 75
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pY line 78
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.cyclicCharacter_pZ line 80
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pX line 82
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pY line 90
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.swap23Character_pZ line 98
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sum_permutedCharacter_pX line 107
Source documentation
Each singleton-leg exponent occurs twice among the first-leg exponents.
```
theorem sum_permutedCharacter_pX :
    (∑ i : Fin 6, (χ.permutedCharacter i).pX) = 2 * (χ.pX + χ.pY + χ.pZ) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character.pX