sub

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

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

Русский

Если A и B Гермитовы, то A - B также Гермитова.

LaTeX

$$$A^{\\ast} = A \\land B^{\\ast} = B \\Rightarrow (A - B)^{\\ast} = A - B$$$

Lean4

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

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

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

Разделы

Аффилиация

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