mul_conjTranspose_self — Mathlib

English

If A.vecMul is injective, then A Aᴴ is positive definite.

Русский

Если A.vecMul инъективна, то A Aᴴ положительно определена.

LaTeX

$$$$ \\operatorname{Injective}(A.\\operatorname{vecMul}) \\Rightarrow \\operatorname{PosDef}(A A^{\\mathrm{H}}). $$$$

Lean4

theorem mul_conjTranspose_self [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R)
    (hA : Function.Injective A.vecMul) : PosDef (A * Aᴴ) := by classical simpa using mul_mul_conjTranspose_same .one hA

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