algebraMap_end_eq_smul_id — Mathlib

English

There is an algebra structure on the endomorphism ring Module.End S M, induced by composition and scalar action, making End(S,M) into an algebra over R.

Русский

Пусть End(S,M) — кольцо эндоморфизмов; существует структура алгебры над R, задаваемая композициями и скалярами.

LaTeX

$$Algebra R (Module.End S M)$$

Lean4

theorem algebraMap_end_eq_smul_id (a : R) : algebraMap R (End S M) a = a • LinearMap.id :=
  rfl

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