unitization

Mathlib.Algebra.Algebra.Subalgebra.Unitization

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.unitization

← MathLib Explorer

English

Auxiliary lemma in the construction of unitization equivalence.

Русский

Вспомог lemma в построении эквивалентности единизации.

LaTeX

$$Lemma in unitization construction$$

Lean4

/-- The natural `R`-algebra homomorphism from the unitization of a non-unital subalgebra into
the algebra containing it. -/
def unitization : Unitization R s →ₐ[R] A :=
  Unitization.lift (NonUnitalSubalgebraClass.subtype s)

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

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

Разделы

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

Аффилиация

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