of_symm_of — Mathlib

English

Repeating the symmetry map returns the original graded tensor's element.

Русский

Повторное применение симметрии возвращает исходный элемент градуированного тензорного произведения.

LaTeX

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

Lean4

@[simp]
theorem of_symm_of (x : A ⊗[R] B) : (of R 𝒜 ℬ).symm (of R 𝒜 ℬ x) = x :=
  rfl

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