piRightHom — Mathlib

English

For all x in A and f in B, piRight(x ⊗ f) = (i ↦ x ⊗ f(i)).

Русский

Для любого x в A и f в ∀ i, B_i, piRight(x ⊗ f) = (i ↦ x ⊗ f(i)).

LaTeX

$$piRight_tmul$$

Lean4

/-- The canonical map `A ⊗[R] (∀ i, B i) →ₐ[S] ∀ i, A ⊗[R] B i`. This is an isomorphism
if `ι` is finite (see `Algebra.TensorProduct.piRight`). -/
def piRightHom : A ⊗[R] (∀ i, B i) →ₐ[S] ∀ i, A ⊗[R] B i :=
  AlgHom.ofLinearMap (_root_.TensorProduct.piRightHom R S A B) (by simp) (by simp)

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