starMap_inl

Mathlib.Algebra.Algebra.Unitization

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

English

Self-adjointness is preserved under the inr embedding to the unitization.

Русский

Самосопряженность сохраняется при вложении inr в единичизацию.

LaTeX

$$$IsSelfAdjoint(a) \iff IsSelfAdjoint(\mathrm{inr}(a))$$$

Lean4

@[simp high]
theorem starMap_inl (φ : A →⋆ₙₐ[R] B) (r : R) : starMap φ (inl r) = algebraMap R (Unitization R B) r := by simp

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

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

Разделы

Аффилиация

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