prodRight_tmul_snd — Mathlib

English

Tensor product commutes with binary products on the right: A ⊗_R (B × C) ≃_S A ⊗_R B × A ⊗_R C.

Русский

Тензорное произведение коммутирует бинарные произведения справа: A ⊗_R (B × C) ≃_S A ⊗_R B × A ⊗_R C.

LaTeX

$$$ A ⊗_R (B × C) \\simeq_S A ⊗_R B × A ⊗_R C $$$

Lean4

@[simp]
theorem prodRight_tmul_snd (a : A) (x : B × C) : (prodRight R S A B C (a ⊗ₜ x)).snd = a ⊗ₜ x.2 :=
  rfl

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