mulLeft — Mathlib

English

For any a ∈ A, the map A → A given by x ↦ a x is an additive and R-linear map; i.e., left multiplication by a is a linear map over R.

Русский

Левое умножение на A-элемент a определяется как линейное отображение A → A над R.

LaTeX

$$mulLeft(R,a) : A →ₗ[R] A, x ↦ a x$$

Lean4

/-- The multiplication on the left in an algebra is a linear map.

Note that this only assumes `SMulCommClass R A A`, so that it also works for `R := Aᵐᵒᵖ`.

When `A` is unital and associative, this is the same as `DistribMulAction.toLinearMap R A a` -/
def mulLeft (a : A) : A →ₗ[R] A where
  toFun := (a * ·)
  map_add' := mul_add _
  map_smul' _ := mul_smul_comm _ _

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