mul_mul_conjTranspose_same — Mathlib

English

If A is PSD, then B A B* is PSD for any B.

Русский

Если A положительно полуопределена, то B A B* положительно полуопределена для любой B.

LaTeX

$$$A \succeq 0 \Rightarrow B A B^* \succeq 0$$$

Lean4

theorem mul_mul_conjTranspose_same {A : Matrix n n R} (hA : PosSemidef A) {m : Type*} [Fintype m] (B : Matrix m n R) :
    PosSemidef (B * A * Bᴴ) := by simpa only [conjTranspose_conjTranspose] using hA.conjTranspose_mul_mul_same Bᴴ

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