conjTranspose_mul_self — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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