gradedComm_one_tmul — Mathlib

English

Braiding interacts compatibly with the unit element in the graded tensor product.

Русский

Брайдинг совместим с единицей в градуированном тензорном произведении.

LaTeX

$$$$ gradedComm_R(\mathcal{A},\mathcal{B})(1 \otimes b) = b \otimes 1. $$$$

Lean4

theorem gradedComm_one_tmul [GradedMonoid.GOne 𝒜] (b : ⨁ i, ℬ i) : gradedComm R 𝒜 ℬ (1 ⊗ₜ b) = b ⊗ₜ 1 :=
  gradedComm_of_zero_tmul _ _ _ _ _

Похожие утверждения