unitization_injective — Mathlib

English

There is a star algebra equivalence between Unitization R s and StarAlgebra.adjoin R (s as set).

Русский

Существует звездное алгебраическое эквивалентство между Unitization R s и StarAlgebra.adjoin.

LaTeX

$$$\mathrm{Unitization}\;R\;s \simeq_{\star[R]} \mathrm{StarAlgebra.adjoin}\;R\,(s)$$$

Lean4

theorem unitization_injective (h1 : (1 : A) ∉ s) : Function.Injective (unitization s) :=
  AlgHomClass.unitization_injective s h1 (unitization s) fun _ ↦ by simp

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