TensorProduct.gradedComm_symm

theorem TensorProduct.gradedComm_symm : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)], (TensorProduct.gradedComm R 𝒜 ℬ).symm = TensorProduct.gradedComm R ℬ 𝒜

The theorem `TensorProduct.gradedComm_symm` states that for any type `R` and a possibly different type for each element `ι`, the commutation (that is, the property of changing the order of the arguments without changing the result) of a graded tensor product is symmetric. This is under the conditions that `ι` forms a commutative semiring, `Additive ℤˣ` is a module over `ι`, the equality of `ι` elements is decidable, `𝒜` and `ℬ` are types dependent on `ι` and each `𝒜 i` and `ℬ i` form an additive commutative group and a module over `R`. Specifically, the theorem asserts that if we swap the roles of `𝒜` and `ℬ` in the tensor product, the property of being a graded commutative tensor product remains unchanged.

More concisely: Given types `R`, `ι` (a commutative semiring), `𝒜` and `ℬ` dependent on `ι` with each `𝒜 i` and `ℬ i` being an additive commutative group and a module over `R`, the graded tensor product of `Additive ℤˣ` over `R` with respect to `𝒜` and then with respect to `ℬ` is equal to the graded tensor product of `Additive ℤˣ` over `R` with respect to `ℬ` and then with respect to `𝒜`.