Finite tensors modulo mutual restriction

Representatives have three natural-number dimensions and coefficients in K. The order is actual linear restriction, and equality in the quotient is mutual restriction. In particular, changing coordinates does not change the class.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : Prop

T is obtained from S by three linear maps on its coordinate spaces.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.refl {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : IsRestriction T T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.trans {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} {P : Type u_7} {Q : Type u_8} {R : Type u_9} [Fintype U] [Fintype V] [Fintype W] [Fintype P] [Fintype Q] [Fintype R] {T : Foundation.Tensor K X Y Z} {S : Foundation.Tensor K U V W} {L : Foundation.Tensor K P Q R} (hTS : IsRestriction T S) (hSL : IsRestriction S L) : IsRestriction T L

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.pullback {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) (fx : U → X) (fy : V → Y) (fz : W → Z) : IsRestriction (Foundation.Tensor.pullback fx fy fz T) T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.of_reindex {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (ex : U ≃ X) (ey : V ≃ Y) (ez : W ≃ Z) : IsRestriction T (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.reindex_iff {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype U] [Fintype V] [Fintype W] [Finite X] [Finite Y] [Finite Z] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) {X' : Type u_10} {Y' : Type u_11} {Z' : Type u_12} {U' : Type u_13} {V' : Type u_14} {W' : Type u_15} [Finite X'] [Finite Y'] [Finite Z'] [Fintype U'] [Fintype V'] [Fintype W'] (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) (eu : U' ≃ U) (ev : V' ≃ V) (ew : W' ≃ W) : IsRestriction (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) (Foundation.Tensor.pullback (⇑eu) (⇑ev) (⇑ew) S) ↔ IsRestriction T S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.product {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} {P : Type u_7} {Q : Type u_8} {R : Type u_9} [Fintype P] [Fintype Q] [Fintype R] {T : Foundation.Tensor K X Y Z} {S : Foundation.Tensor K U V W} {T' : Foundation.Tensor K P Q R} {U' : Type u_10} {V' : Type u_11} {W' : Type u_12} [Fintype U'] [Fintype V'] [Fintype W'] {S' : Foundation.Tensor K U' V' W'} (hT : IsRestriction T T') (hS : IsRestriction S S') : IsRestriction (T.product S) (T'.product S')

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.sum {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} {P : Type u_7} {Q : Type u_8} {R : Type u_9} [Fintype P] [Fintype Q] [Fintype R] {T : Foundation.Tensor K X Y Z} {S : Foundation.Tensor K U V W} {T' : Foundation.Tensor K P Q R} {U' : Type u_10} {V' : Type u_11} {W' : Type u_12} [Fintype U'] [Fintype V'] [Fintype W'] {S' : Foundation.Tensor K U' V' W'} (hT : IsRestriction T T') (hS : IsRestriction S S') : IsRestriction (sumTensor T S) (sumTensor T' S')

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.zero {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype U] [Fintype V] [Fintype W] (S : Foundation.Tensor K U V W) : IsRestriction 0 S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.rank_le {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] {T : Foundation.Tensor K X Y Z} {S : Foundation.Tensor K U V W} (h : IsRestriction T S) : exactRank T ≤ exactRank S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.eq_zero_of_zero {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype U] [Fintype V] [Fintype W] {T : Foundation.Tensor K X Y Z} (h : IsRestriction T 0) : T = 0

structure MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor (K : Type) : Type

A set-sized presentation of any finite coefficient tensor over K.

• nx : ℕ

  Dimension of the tensor's first coordinate space.

• ny : ℕ

  Dimension of the tensor's second coordinate space.

• nz : ℕ

  Dimension of the tensor's third coordinate space.

• coeff : Foundation.Tensor K (Fin self.nx) (Fin self.ny) (Fin self.nz)

  Coefficient array in the three standard finite coordinate spaces.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor {K : Type} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : FiniteTensor K

Replace arbitrary finite coordinate sets by standard finite sets.

Equations

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

@[instance_reducible]

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.instLE {K : Type} [Field K] : LE (FiniteTensor K)

Equations

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

@[instance_reducible]

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.instPreorder {K : Type} [Field K] : Preorder (FiniteTensor K)

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor_le_iff {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : ofTensor T ≤ ofTensor S ↔ IsRestriction T S

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.product {K : Type} [Field K] (T S : FiniteTensor K) : FiniteTensor K

Tensor product represented again on standard finite coordinate sets.

Equations

• T.product S = MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor (T.coeff.product S.coeff)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.sum {K : Type} [Field K] (T S : FiniteTensor K) : FiniteTensor K

Direct sum represented again on standard finite coordinate sets.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.product_mono {K : Type} [Field K] {T T' S S' : FiniteTensor K} (hT : T ≤ T') (hS : S ≤ S') : T.product S ≤ T'.product S'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.sum_mono {K : Type} [Field K] {T T' S S' : FiniteTensor K} (hT : T ≤ T') (hS : S ≤ S') : T.sum S ≤ T'.sum S'

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass (K : Type) [Field K] : Type

Finite tensors over K, with two presentations identified exactly when each is a linear restriction of the other.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass {K : Type} [Field K] (T : FiniteTensor K) : TensorClass K

The class of a finite tensor presentation.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_eq_iff {K : Type} [Field K] (T S : FiniteTensor K) : tensorClass T = tensorClass S ↔ T ≤ S ∧ S ≤ T

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_le_iff {K : Type} [Field K] (T S : FiniteTensor K) : tensorClass T ≤ tensorClass S ↔ T ≤ S

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : TensorClass K

The quotient class of a tensor on any three finite coordinate sets.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_le_iff {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : classOf T ≤ classOf S ↔ IsRestriction T S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_iff {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : classOf T = classOf S ↔ IsRestriction T S ∧ IsRestriction S T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_reindex {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (ex : U ≃ X) (ey : V ≃ Y) (ez : W ≃ Z) : classOf (Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) T) = classOf T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_of_reindex {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] {T : Foundation.Tensor K X Y Z} {S : Foundation.Tensor K U V W} (ex : X ≃ U) (ey : Y ≃ V) (ez : Z ≃ W) (h : Foundation.Tensor.pullback (⇑ex) (⇑ey) (⇑ez) S = T) : classOf T = classOf S

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_coeff {K : Type} [Field K] (T : FiniteTensor K) : classOf T.coeff = tensorClass T

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instMulTensorClass {K : Type} [Field K] : Mul (TensorClass K)

Equations

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

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instAddTensorClass {K : Type} [Field K] : Add (TensorClass K)

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_product {K : Type} [Field K] (T S : FiniteTensor K) : tensorClass T * tensorClass S = tensorClass (T.product S)

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_sum {K : Type} [Field K] (T S : FiniteTensor K) : tensorClass T + tensorClass S = tensorClass (T.sum S)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_product {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : classOf (T.product S) = classOf T * classOf S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_sum {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {U : Type u_4} {V : Type u_5} {W : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : classOf (sumTensor T S) = classOf T + classOf S

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instZeroTensorClass {K : Type} [Field K] : Zero (TensorClass K)

Equations

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

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instOneTensorClass {K : Type} [Field K] : One (TensorClass K)

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_zero {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] : classOf 0 = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_assoc {K : Type} [Field K] (a b c : TensorClass K) : a + b + c = a + (b + c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_comm {K : Type} [Field K] (a b : TensorClass K) : a + b = b + a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_zero {K : Type} [Field K] (a : TensorClass K) : a + 0 = a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_zero_add {K : Type} [Field K] (a : TensorClass K) : 0 + a = a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_assoc {K : Type} [Field K] (a b c : TensorClass K) : a * b * c = a * (b * c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_comm {K : Type} [Field K] (a b : TensorClass K) : a * b = b * a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_one {K : Type} [Field K] (a : TensorClass K) : a * 1 = a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_one_mul {K : Type} [Field K] (a : TensorClass K) : 1 * a = a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_zero {K : Type} [Field K] (a : TensorClass K) : a * 0 = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_zero_mul {K : Type} [Field K] (a : TensorClass K) : 0 * a = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_left_distrib {K : Type} [Field K] (a b c : TensorClass K) : a * (b + c) = a * b + a * c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_right_distrib {K : Type} [Field K] (a b c : TensorClass K) : (a + b) * c = a * c + b * c

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instCommSemiringTensorClass {K : Type} [Field K] : CommSemiring (TensorClass K)

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.mul_mono {K : Type} [Field K] {T T' S S' : TensorClass K} (hT : T ≤ T') (hS : S ≤ S') : T * S ≤ T' * S'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.add_mono {K : Type} [Field K] {T T' S S' : TensorClass K} (hT : T ≤ T') (hS : S ≤ S') : T + S ≤ T' + S'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.zero_le {K : Type} [Field K] (T : TensorClass K) : 0 ≤ T

Every tensor class is nonnegative in the restriction order.

@[instance_reducible]

noncomputable instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instOrderBotTensorClass {K : Type} [Field K] : OrderBot (TensorClass K)

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instOrderBotTensorClass = { bot := 0, bot_le := ⋯ }

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instIsOrderedAddMonoidTensorClass {K : Type} [Field K] : IsOrderedAddMonoid (TensorClass K)

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instIsOrderedMonoidTensorClass {K : Type} [Field K] : IsOrderedMonoid (TensorClass K)

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instIsOrderedRingTensorClass {K : Type} [Field K] : IsOrderedRing (TensorClass K)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank {K : Type} [Field K] : TensorClass K → ℕ

Exact rank descends to mutual-restriction classes.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_tensorClass {K : Type} [Field K] (T : FiniteTensor K) : rank (tensorClass T) = exactRank T.coeff

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_classOf {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : rank (classOf T) = exactRank T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_mono {K : Type} [Field K] {T S : TensorClass K} (h : T ≤ S) : rank T ≤ rank S

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_mul_le {K : Type} [Field K] (T S : TensorClass K) : rank (T * S) ≤ rank T * rank S

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass (K : Type) [Field K] (n : ℕ) : TensorClass K

Square matrix multiplication as an element of the tensor semiring.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_matrixClass {K : Type} [Field K] (n : ℕ) : rank (matrixClass K n) = exactMatrixRank K n

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_mul {K : Type} [Field K] (m n : ℕ) : matrixClass K (m * n) = matrixClass K m * matrixClass K n

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_one {K : Type} [Field K] : matrixClass K 1 = 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_pow {K : Type} [Field K] (m j : ℕ) : matrixClass K (m ^ j) = matrixClass K m ^ j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_zero_iff {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (T : Foundation.Tensor K X Y Z) : classOf T = 0 ↔ T = 0

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.instNontrivialTensorClass {K : Type} [Field K] : Nontrivial (TensorClass K)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.one_le_classOf_of_ne_zero {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} (hT : T ≠ 0) : 1 ≤ classOf T

A nonzero tensor has a nonzero coefficient, which restricts to scalar multiplication.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.one_le_of_ne_zero {K : Type} [Field K] {T : TensorClass K} (hT : T ≠ 0) : 1 ≤ T

Every nonzero class dominates the multiplicative unit.