add

Mathlib.LinearAlgebra.Matrix.Hermitian

URI: https://scilib.ai/kg/mathlib#Matrix.IsHermitian.add

English

If A and B are Hermitian, then A + B is Hermitian.

Русский

Если A и B эрмитовы, то их сумма эрмитова.

LaTeX

$$$A.IsHermitian \to B.IsHermitian \to (A + B).IsHermitian$$$

Lean4

@[simp]
theorem add {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) : (A + B).IsHermitian :=
  IsSelfAdjoint.add hA hB

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

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

Разделы

Аффилиация

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