Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.cyclic {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} (T : Tensor K X Y Z) : Tensor K Y Z X

Rotate a tensor's three coordinate spaces cyclically.

Equations

• T.cyclic y z x = T x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.cyclic {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {T : Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) : T.cyclic.RankAtMost r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSumProductEquiv (ι : Type u_8) (κ : Type u_9) (X : Type u_10) (U : Type u_11) : (ι × κ) × X × U ≃ (ι × X) × κ × U

Reassociate summand tags and coordinates when distributing a tensor product over direct sums.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSumProduct {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] {ι : Type u_8} {κ : Type u_9} [DecidableEq ι] [DecidableEq κ] (T : ι → Tensor K X Y Z) (S : κ → Tensor K U V W) : pullback (⇑(directSumProductEquiv ι κ X U)) (⇑(directSumProductEquiv ι κ Y V)) (⇑(directSumProductEquiv ι κ Z W)) ((directSum T).product (directSum S)) = directSum fun (i : ι × κ) => (T i.1).product (S i.2)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSumProduct {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [CommSemiring K] {ι : Type u_8} {κ : Type u_9} [DecidableEq ι] [DecidableEq κ] {T : ι → Tensor K X Y Z} {S : κ → Tensor K U V W} {r s : ℕ} (hT : (directSum T).RankAtMost r) (hS : (directSum S).RankAtMost s) : (directSum fun (i : ι × κ) => (T i.1).product (S i.2)).RankAtMost (r * s)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSumPullback {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} {X' : Type u_9} {Y' : Type u_10} {Z' : Type u_11} [DecidableEq ι] (T : ι → Tensor K X Y Z) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : pullback (fun (x : ι × X') => (x.1, fx x.2)) (fun (y : ι × Y') => (y.1, fy y.2)) (fun (z : ι × Z') => (z.1, fz z.2)) (directSum T) = directSum fun (i : ι) => pullback fx fy fz (T i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSumPullback {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} {X' : Type u_9} {Y' : Type u_10} {Z' : Type u_11} [DecidableEq ι] {T : ι → Tensor K X Y Z} {r : ℕ} (h : (directSum T).RankAtMost r) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (directSum fun (i : ι) => Tensor.pullback fx fy fz (T i)).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.cyclic_directSum {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : ι → Tensor K X Y Z) : (directSum T).cyclic = directSum fun (i : ι) => (T i).cyclic

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSumCyclic {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] {T : ι → Tensor K X Y Z} {r : ℕ} (h : (directSum T).RankAtMost r) : (directSum fun (i : ι) => (T i).cyclic).RankAtMost r

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSumPowerEquiv (ι : Type u_8) (X : Type u_9) (n : ℕ) : (Fin n → ι) × (Fin n → X) ≃ (Fin n → ι × X)

Identify paired words with words of paired summand tags and coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : ι → Tensor K X Y Z) (n : ℕ) : pullback (⇑(directSumPowerEquiv ι X n)) (⇑(directSumPowerEquiv ι Y n)) (⇑(directSumPowerEquiv ι Z n)) ((directSum T).power n) = directSum fun (f : Fin n → ι) (x : Fin n → X) (y : Fin n → Y) (z : Fin n → Z) => ∏ i : Fin n, T (f i) (x i) (y i) (z i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_const_power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] (T : Tensor K X Y Z) (n : ℕ) : pullback (⇑(directSumPowerEquiv ι X n)) (⇑(directSumPowerEquiv ι Y n)) (⇑(directSumPowerEquiv ι Z n)) ((directSum fun (x : ι) => T).power n) = directSum fun (x : Fin n → ι) => T.power n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_of_power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] {T : Tensor K X Y Z} {n R : ℕ} (h : ((directSum fun (x : ι) => T).power n).RankAtMost R) : (directSum fun (x : Fin n → ι) => T.power n).RankAtMost R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.directSum_const_power {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring K] {ι : Type u_8} [DecidableEq ι] {T : Tensor K X Y Z} {r : ℕ} (h : (directSum fun (x : ι) => T).RankAtMost r) (n : ℕ) : (directSum fun (x : Fin n → ι) => T.power n).RankAtMost (r ^ n)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareX (A : Type u_11) (B : Type u_12) (C : Type u_13) : (A × B × C) × A × B × C ≃ ((A × B) × B × C) × C × A

First-leg coordinate permutation combining three cyclic rectangular tensors into a square tensor.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareY (A : Type u_11) (B : Type u_12) (C : Type u_13) : (A × B × C) × A × B × C ≃ ((B × C) × C × A) × A × B

Second-leg coordinate permutation combining three cyclic rectangular tensors into a square tensor.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.rectangularSquareZ (A : Type u_11) (B : Type u_12) (C : Type u_13) : (A × B × C) × A × B × C ≃ ((C × A) × A × B) × B × C

Third-leg coordinate permutation combining three cyclic rectangular tensors into a square tensor.

Equations

• One or more equations did not get rendered due to their size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_rank_of_power {K : Type u_1} [CommSemiring K] {A : Type u_8} {B : Type u_9} {C : Type u_10} [DecidableEq A] [DecidableEq B] [DecidableEq C] {ι : Type u_11} [DecidableEq ι] {n R : ℕ} (h : ((directSum fun (x : ι) => matrixCoefficients A B C).power n).RankAtMost R) : (directSum fun (x : Fin n → ι) => matrixCoefficients (Fin n → A) (Fin n → B) (Fin n → C)).RankAtMost R

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_cyclic_product_square {K : Type u_1} [CommSemiring K] {A : Type u_8} {B : Type u_9} {C : Type u_10} [DecidableEq A] [DecidableEq B] [DecidableEq C] : pullback (⇑(rectangularSquareX A B C)) (⇑(rectangularSquareY A B C)) (⇑(rectangularSquareZ A B C)) (((matrixCoefficients A B C).product (matrixCoefficients B C A)).product (matrixCoefficients C A B)) = matrixCoefficients (A × B × C) (A × B × C) (A × B × C)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.cyclic_matrixCoefficients {K : Type u_1} [CommSemiring K] {A : Type u_8} {B : Type u_9} {C : Type u_10} [DecidableEq A] [DecidableEq B] [DecidableEq C] : (matrixCoefficients A B C).cyclic = matrixCoefficients B C A

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_symmetrized_rank {K : Type u_1} [CommSemiring K] {A : Type u_8} {B : Type u_9} {C : Type u_10} [DecidableEq A] [DecidableEq B] [DecidableEq C] {r : ℕ} (h : (matrixCoefficients A B C).RankAtMost r) : (matrixCoefficients (A × B × C) (A × B × C) (A × B × C)).RankAtMost (r ^ 3)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixCoefficients_directSum_symmetrized_rank {K : Type u_1} [CommSemiring K] {A : Type u_8} {B : Type u_9} {C : Type u_10} [DecidableEq A] [DecidableEq B] [DecidableEq C] {ι : Type u_11} [DecidableEq ι] {r : ℕ} (h : (directSum fun (x : ι) => matrixCoefficients A B C).RankAtMost r) : (directSum fun (x : (ι × ι) × ι) => matrixCoefficients (A × B × C) (A × B × C) (A × B × C)).RankAtMost (r ^ 3)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.symmetrized_tag_card (ι : Type u_11) [Fintype ι] : Fintype.card ((ι × ι) × ι) = Fintype.card ι ^ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.symmetrized_index_card {A : Type u_8} {B : Type u_9} {C : Type u_10} [Fintype A] [Fintype B] [Fintype C] : Fintype.card (A × B × C) = Fintype.card A * Fintype.card B * Fintype.card C