add

Mathlib.Algebra.Star.SelfAdjoint

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

← MathLib Explorer

English

The sum of two self-adjoint elements is self-adjoint.

Русский

Сумма двух самосопряжённых элементов самосопряжена.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \text{IsSelfAdjoint}(y) \rightarrow \text{IsSelfAdjoint}(x + y)$$$

Lean4

@[aesop 90% apply]
theorem add {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x + y) := by
  simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]

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

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

Разделы

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

Аффилиация

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