symm_of_of — Mathlib

English

The symmetry map on graded tensor products is the inverse of itself, i.e., applying it to any element recovers the original.

Русский

Симметрия градуированного тензорного произведения сама по себе обратна, то есть применение к элементу возвращает исходный.

LaTeX

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

Lean4

@[simp]
theorem symm_of_of (x : 𝒜 ᵍ⊗[R] ℬ) : of R 𝒜 ℬ ((of R 𝒜 ℬ).symm x) = x :=
  rfl

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