tmul_eq_smul_one_tmul — Mathlib

English

The canonical bilinear map mk: M × N → M ⊗_R N sends (m,n) to m ⊗ n.

Русский

Каноническое билинеарное отображение mk: M × N → M ⊗_R N отправляет (m,n) в m ⊗ n.

LaTeX

$$$\text{mk}: M \times N \to M \otimes_R N$ with $\text{mk}(m,n) = m \otimes n$$$

Lean4

theorem tmul_eq_smul_one_tmul {S : Type*} [Semiring S] [Module R S] [SMulCommClass R S S] (s : S) (m : M) :
    s ⊗ₜ[R] m = s • (1 ⊗ₜ[R] m) := by nth_rw 1 [← mul_one s, ← smul_eq_mul, smul_tmul']

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