lmul_algebraMap — Mathlib

English

For any x in R, left multiplication by the image of x under the algebra map equals the scalar smul by x, i.e., lmul_R,A(algebraMap_R,A(x)) = lsmul_R,R,A(x).

Русский

Для любого x в R левое умножение на образ x через алгебраическую аппроксимацию совпадает с умножением скаляра: lmul(R,A)(algebraMap_R,A(x)) = lsmul_R,R,A(x).

LaTeX

$$$\mathrm{lmul}_{R,A}(\mathrm{algebraMap}_{R,A}(x)) = \mathrm{lsmul}_{R,R,A}(x)$$$

Lean4

theorem lmul_algebraMap (x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R R A x :=
  Eq.symm <| LinearMap.ext <| smul_def x

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