Theorems · Theorem · ring theory

TensorProduct.tmul_of_gradedMul_of_tmul

∀ (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)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (j₁ i₂ : ι) (a₁ : DirectSum ι fun i => 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂)
  (b₂ : DirectSum ι fun i => ℬ i),
  ((TensorProduct.gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) =
    (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.External

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringModuleDecidableEqCommRingAddCommGroupAddCommGroupModuleModuleDirectSum.GRingDirectSum.GRingDirectSum.GAlgebraDirectSum.GAlgebra