liftAddHom_tmul — Mathlib

English

Scalar action can be moved across the tensor product: (r · m) ⊗ n = m ⊗ (r · n).

Русский

Действие скаляра можно переносить через тензор: (r · m) ⊗ n = m ⊗ (r · n).

LaTeX

$$$ (r \\cdot m) \\otimes_R n = m \\otimes_R (r \\cdot n). $$$

Lean4

@[simp]
theorem liftAddHom_tmul (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), f (r • m) n = f m (r • n)) (m : M) (n : N) :
    liftAddHom f hf (m ⊗ₜ n) = f m n :=
  rfl

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