smul_tmul — Mathlib

English

In the extended scalar module, the scalar action distributes as s · (s' ⊗ m) = (s s') ⊗ m for s, s' in S and m in M.

Русский

В модуле расширения скаляров скалярная операция удовлетворяет: s · (s' ⊗ m) = (s s') ⊗ m, для любых s, s' ∈ S и m ∈ M.

LaTeX

$$$s \cdot (s' \otimes_{R,f} m) = (s s') \otimes_{R,f} m$$$

Lean4

@[simp]
protected theorem smul_tmul {M : ModuleCat.{v} R} (s s' : S) (m : M) :
    s • (s' ⊗ₜ[R,f] m : (extendScalars f).obj M) = (s * s') ⊗ₜ[R,f] m :=
  rfl

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