map_adjoin_singleton

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgHom.map_adjoin_singleton

← MathLib Explorer

English

General version of map_adjoin for arbitrary f, s.

Русский

Обобщённая версия map_adjoin для произвольной пары f и s.

LaTeX

$$$\operatorname{map}_f(\operatorname{adjoin}_R(s)) = \operatorname{adjoin}_R (f''s)$$$

Lean4

@[simp]
theorem _root_.NonUnitalAlgHom.map_adjoin_singleton [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (x : A) :
    map f (adjoin R { x }) = adjoin R {f x} := by simp [NonUnitalAlgHom.map_adjoin]

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

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

Разделы

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

Аффилиация

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