fromBlocks — Mathlib

English

A block matrix fromBlocks A B C D is Hermitian if A and D are Hermitian and Bᴴ = C.

Русский

Блочная матрица fromBlocks A B C D эрмитова, если A и D эрмитовы, а Bᴴ = C.

LaTeX

$$If A.IsHermitian, Bᴴ = C, and D.IsHermitian, then (A.fromBlocks B C D).IsHermitian$$

Lean4

/-- A block matrix `A.from_blocks B C D` is Hermitian,
if `A` and `D` are Hermitian and `Bᴴ = C`. -/
theorem fromBlocks {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} (hA : A.IsHermitian)
    (hBC : Bᴴ = C) (hD : D.IsHermitian) : (A.fromBlocks B C D).IsHermitian :=
  by
  have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
  unfold Matrix.IsHermitian
  rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]

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