of_symm_one — Mathlib

English

The symmetry map on graded tensor product is its own inverse on the level of elements.

Русский

Свойство симметрии на градуированном тензорном произведении означает, что симметрия — это собственный обратный отображение на уровне элементов.

LaTeX

$$$$ (\text{of }R,\mathcal{A},\mathcal{B}).symm( (\text{of }R,\mathcal{A},\mathcal{B}) (x) ) = x. $$$$

Lean4

@[simp]
theorem of_symm_one : (of R 𝒜 ℬ).symm 1 = 1 :=
  rfl

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