Finite coefficient tensors and their algebraic transformations.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.card_le_of_identity {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field K] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {T : Tensor K X Y Z} {r : ℕ} (hT : T.RankAtMost r) (x : ι → X) (y : ι → Y) (z : ι → Z) (hidentity : ∀ (i j : ι), T (x i) (y i) (z j) = if i = j then 1 else 0) : Fintype.card ι ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_matrixCoefficients_rank_lower {K : Type u_1} [Field K] {Label : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [Fintype Label] [Fintype A] [Fintype C] [DecidableEq Label] [DecidableEq A] [DecidableEq B] [DecidableEq C] [Nonempty B] {r : ℕ} (h : (directSum fun (x : Label) => matrixCoefficients A B C).RankAtMost r) : Fintype.card Label * (Fintype.card C * Fintype.card A) ≤ r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.directSum_square_rank_lower {K : Type u_1} [Field K] (k n r : ℕ) (hn : 0 < n) (h : (directSum fun (x : Fin k) => matrixCoefficients (Fin n) (Fin n) (Fin n)).RankAtMost r) : k * n ^ 2 ≤ r