Finite coefficient tensors and their algebraic transformations.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.FieldCoefficientExtraction.coeff_triple {F : Type u_1} [CommSemiring F] (a b c : Polynomial F) (d : ℕ) : (a * b * c).coeff d = ∑ i : Fin (d + 1), ∑ j : Fin (d + 1), (if ↑j ≤ d - ↑i then a.coeff (d - ↑i - ↑j) else 0) * b.coeff ↑j * c.coeff ↑i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.FieldCoefficientExtraction.rankAtMost_coeff {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [CommSemiring F] {P : Foundation.Tensor (Polynomial F) X Y Z} {r : ℕ} (hP : P.RankAtMost r) (d : ℕ) : Foundation.Tensor.RankAtMost (fun (x : X) (y : Y) (z : Z) => (P x y z).coeff d) ((d + 1) ^ 2 * r)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.FieldCoefficientExtraction.rank_power {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Foundation.Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (n : ℕ) : (T.power n).RankAtMost ((d * n + 1) ^ 2 * r ^ n)