of_algebraMap_smul

Mathlib.Algebra.Algebra.Tower

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

← MathLib Explorer

English

If 1 ∉ s, then the unitization map is injective.

Русский

Если 1 не принадлежит s, отображение единичизации инъективно.

LaTeX

$$$\text{If } 1 \notin s,\quad \text{unitization}(s)\text{ is injective}$$$

Lean4

theorem of_algebraMap_smul [SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) : IsScalarTower R A M where
  smul_assoc r a x := by rw [Algebra.smul_def, mul_smul, h]

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

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

Разделы

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

Аффилиация

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