map_adjoin_singleton

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

← MathLib Explorer

English

The coe of the top subalgebra equals the universe of the ambient algebra.

Русский

Приведение вершины подалгебры совпадает с множеством всего алгебра-окружения.

LaTeX

$$$↑(\\top) = A$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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