piRight_symm_single — Mathlib

English

There is an isomorphism piRightHom: N ⊗_R (ι → R) ≃_S (ι → N) and its explicit tmul rules.

Русский

Существует изоморфизм piRightHom: N ⊗_R (ι → R) ≃_S (ι → N) и явные правила на tmul.

LaTeX

$$$piRightHom : N \otimes_R (\iota \to R) \cong_S (\iota \to N).$$$

Lean4

@[simp]
theorem piRight_symm_single (x : N) (i : ι) (m : M i) :
    (piRight R S N M).symm (Pi.single i (x ⊗ₜ m)) = x ⊗ₜ Pi.single i m := by simp [piRight]

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