directLimitRight_symm_of_tmul — Mathlib

English

The inverse of directLimitRight acts on a simple tensor by swapping factors and inserting the inverse sign accordingly.

Русский

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

LaTeX

$$$\mathrm{directLimitRight}\;\text{symm}\;\text{of}\ (m \otimes g) = m \otimes \text{in}_i(g)$$$

Lean4

@[simp]
theorem directLimitRight_symm_of_tmul {i : ι} (m : M) (g : G i) :
    (directLimitRight f M).symm (of _ _ _ _ _ (m ⊗ₜ g)) = m ⊗ₜ of _ _ _ f _ g := by
  simp [directLimitRight, congr_symm_apply_of]

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