algebraMap_eq_smul_one'

Mathlib.Algebra.Algebra.Defs

URI: https://scilib.ai/kg/mathlib#Algebra.algebraMap_eq_smul_one'

English

The algebra map is the same as smul_one, i.e., algebraMap R A equals the function r ↦ r • 1.

Русский

Алгебраически отображение совпадает со smul_one: algebraMap R A = (\lambda r. r • 1).

LaTeX

$$$\operatorname{algebraMap}(R,A) = \lambda r. r \cdot 1_A$$$

Lean4

theorem algebraMap_eq_smul_one' : ⇑(algebraMap R A) = fun r => r • (1 : A) :=
  funext algebraMap_eq_smul_one

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru