fromBlocks — Mathlib

English

A block matrix A.fromBlocks B C D is symmetric if A and D are symmetric and B^T = C.

Русский

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

LaTeX

$$$A^{T}=A,\ D^{T}=D,\ B^{T}=C\ \Longrightarrow\ (A.fromBlocks B C D)^{T}=(A.fromBlocks B C D)\,.$$$

Lean4

/-- A block matrix `A.fromBlocks B C D` is symmetric,
if `A` and `D` are symmetric and `Bᵀ = C`. -/
theorem fromBlocks {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} (hA : A.IsSymm)
    (hBC : Bᵀ = C) (hD : D.IsSymm) : (A.fromBlocks B C D).IsSymm :=
  by
  have hCB : Cᵀ = B := by
    rw [← hBC]
    simp
  unfold Matrix.IsSymm
  rw [fromBlocks_transpose, hA, hCB, hBC, hD]

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