isometry_inr

Mathlib.Analysis.Normed.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.isometry_inr

English

Under RegularNormedAlgebra, splitMul 𝕜 A is injective.

Русский

При RegularNormedAlgebra 𝕜 A отображение splitMul 𝕜 A инъективно.

LaTeX

$$$$\\text{Injective}(splitMul\\ 𝕜 A).$$$$

Lean4

theorem isometry_inr : Isometry ((↑) : A → Unitization 𝕜 A) :=
  AddMonoidHomClass.isometry_of_norm (inrNonUnitalAlgHom 𝕜 A) norm_inr

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

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

Разделы

Аффилиация

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