rid_tmul — Mathlib

English

For any r in R and a in M, the rid map applied to the simple tensor a ⊗ r yields the scalar action r • a.

Русский

Для любого элемента r ∈ R и a ∈ M отображение rid на простом тензоре a ⊗ r даёт действие скаляра: r • a.

LaTeX

$$$ (Coalgebra.TensorProduct.rid \ R \, S \, M)(a \otimes_{\mathrm{t}} r) = r \cdot a $$$

Lean4

@[simp]
theorem rid_tmul (r : R) (a : M) : Coalgebra.TensorProduct.rid R S M (a ⊗ₜ r) = r • a :=
  rfl

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