English
For every element b in A, the map x ↦ x b is linear over R (i.e., right multiplication by a fixed element is an R-linear map).
Русский
Для каждого элемента b ∈ A отображение x ↦ x b является линейным относительно R (правое умножение на фиксированное значение является линейным отображением по R).
LaTeX
$$$$ \forall b \in A, \quad \forall x,y \in A, \ (x+y)b = xb+yb \quad\text{and}\quad \forall r \in R,\ \forall x \in A,\ (r x)b = r(xb). $$$$
Lean4
/-- The multiplication on the right in an algebra is a linear map.
Note that this only assumes `IsScalarTower 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 (MulOpposite.op b)`. -/
def mulRight (b : A) : A →ₗ[R] A where
toFun := (· * b)
map_add' _ _ := add_mul _ _ _
map_smul' _ _ := smul_mul_assoc _ _ _
