ofLinearMap_id — Mathlib

English

toEnd maps an algebra endomorphism to a module endomorphism, i.e., it is a monoid homomorphism from AlgHom(R,A,A) to Module.End(R,A).

Русский

toEnd переводит алгебраический эндоморфизм в концевой линейный отображение; это моноидоморфизм.

LaTeX

$$$$ \mathrm{toEnd}: \mathrm{AlgHom}(R,A,A) \to^* \mathrm{Module.End}(R,A). $$$$

Lean4

@[simp]
theorem ofLinearMap_id (map_one) (map_mul) : ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A :=
  rfl

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