inr

Mathlib.Algebra.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#IsSelfAdjoint.inr

English

Inr preserves self-adjointness via the star operation.

Русский

Inr сохраняет самосопряжённость через операцию звезды.

LaTeX

$$IsSelfAdjoint.inr : IsSelfAdjoint a → IsSelfAdjoint (a : Unitization R A)$$

Lean4

theorem _root_.IsSelfAdjoint.inr (ha : IsSelfAdjoint a) : IsSelfAdjoint (a : Unitization R A) :=
  isSelfAdjoint_inr.mpr ha

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

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

Разделы

Аффилиация

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