Theorems · Theorem · ring theory

TensorProduct.gradedComm_symm

∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [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 braiding is symmetric.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.External

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringModuleDecidableEqCommRingAddCommGroupAddCommGroupModuleModule