gradedComm_symm — Mathlib

English

The braiding operation is symmetric; swapping the two factors twice returns to the original configuration.

Русский

Браидинг-операция симметрична; дважды поменяв местами факторы, получаем исходную конфигурацию.

LaTeX

$$$$ (gradedComm_R(\mathcal{A},\mathcal{B}))^{\mathrm{symm}} = gradedComm_R(\mathcal{B},\mathcal{A}). $$$$

Lean4

/-- The braiding is symmetric. -/
@[simp]
theorem gradedComm_symm : (gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜 := by rfl

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