eq_sqrt_iff_sq_eq — Mathlib

English

If A is positive semidefinite and B is positive semidefinite, then A = sqrt(B) iff A^2 = B.

Русский

Если A и B положительно полуопределены, то A = sqrt(B) тогда и только тогда, когда A^2 = B.

LaTeX

$$$A^{PosSemidef} \land B^{PosSemidef} \Rightarrow (A = \sqrt{B}) \iff (A^{2} = B).$$$

Lean4

@[deprecated CFC.sqrt_eq_iff (since := "2025-09-23")]
theorem eq_sqrt_iff_sq_eq {B : Matrix n n 𝕜} (hB : PosSemidef B) : A = CFC.sqrt B ↔ A ^ 2 = B := by
  rw [eq_comm, CFC.sqrt_eq_iff B A hB.nonneg hA.nonneg, sq]

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