commute_iff — Mathlib

English

A matrix is positive definite if and only if it equals B^H B for some invertible B.

Русский

Матрица положительно определена тогда и только тогда, когда она равна B^H B для некоторой обратимой B.

LaTeX

$$$\text{PosDef}(A) \iff \exists B:\text{Matrix}, \ IsUnit(B) \land A = B^H B.$$$

Lean4

theorem commute_iff {A B : Matrix n n 𝕜} (hA : A.PosDef) (hB : B.PosDef) : Commute A B ↔ (A * B).PosDef := by
  classical
  rw [commute_iff_mul_nonneg hA.posSemidef.nonneg hB.posSemidef.nonneg, nonneg_iff_posSemidef]
  exact ⟨fun h => h.posDef_iff_isUnit.mpr <| hA.isUnit.mul hB.isUnit, fun h => h.posSemidef⟩

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