algebraMap_smul

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#IsScalarTower.algebraMap_smul

← MathLib Explorer

English

The range of unitization equals the StarAlgebra.adjoin generated by s.

Русский

Образ единичизации равен StarAlgebra.adjoin, порожденному s.

LaTeX

$$$\mathrm{range}(\mathrm{unitization}\;s) = \mathrm{StarAlgebra.adjoin}\;R\;s$$$

Lean4

theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) : algebraMap R A r • x = r • x := by
  rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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