lmul' — Mathlib

English

The linear map lmul' corresponds to multiplication by the left factor via the canonical tensor product map.

Русский

Линейное отображение lmul' соответствует умножению слева через каноническое отображение тензорного произведения.

LaTeX

$$lmul'_toLinearMap$$

Lean4

/-- `LinearMap.mul'` as an `AlgHom` over the base ring. -/
def lmul' : S ⊗[R] S →ₐ[R] S :=
  (lmul'' R).restrictScalars R

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