mul_single_one_apply — Mathlib

English

Left multiplication by the basis element with unit coefficient acts by scalar: (single 1 r) * x evaluated at m equals r · x(m).

Русский

Левое умножение на базисный элемент с единичным коэффициентом действует как умножение на скаляра: (single 1 r) * x по M равно r · x(M).

LaTeX

$$$ (\operatorname{single}(1,r) * x)(m) = r \cdot x(m) $$$

Lean4

@[to_additive (dont_translate := R) mul_single_zero_apply]
theorem mul_single_one_apply (x : MonoidAlgebra R M) (r : R) (m : M) :
    (x * single 1 r : MonoidAlgebra R M) m = x m * r :=
  x.mul_single_apply_aux (by simp)

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