gradedComm_tmul_one — Mathlib

English

Swapping a tensor with 1 in the second factor yields the same as placing 1 in the first factor and swapping.

Русский

Перестановка тензора с единицей во втором факторе эквивалентна переносу единицы в первый фактор и перестановке.

LaTeX

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

Lean4

theorem gradedComm_tmul_one [GradedMonoid.GOne ℬ] (a : ⨁ i, 𝒜 i) : gradedComm R 𝒜 ℬ (a ⊗ₜ 1) = 1 ⊗ₜ a :=
  gradedComm_tmul_of_zero _ _ _ _ _

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