gradedComm_one — Mathlib

English

Applying gradedComm to a tensor of an element with an algebra map yields the algebra map on the swapped side.

Русский

Применение gradedComm к тензору элемента и образа по алгебраическому отображению даёт образ по алгебраическому отображению на обратной стороне.

LaTeX

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

Lean4

@[simp]
theorem gradedComm_one [DirectSum.GSemiring 𝒜] [DirectSum.GSemiring ℬ] : gradedComm R 𝒜 ℬ 1 = 1 :=
  gradedComm_one_tmul _ _ _ _

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