English
For A PSD and any B PSD, A^2 = B^2 iff A = B.
Русский
Для PSD A и B: A^2 = B^2 тогда и только тогда, когда A = B.
LaTeX
$$∀ {A B} (hA : A.PosSemidef) (hB : B.PosSemidef), A^2 = B^2 ⇔ A = B.$$
Lean4
/-- A positive semi-definite matrix is positive definite if and only if it is invertible. -/
@[grind =]
theorem posDef_iff_isUnit [DecidableEq n] {x : Matrix n n 𝕜} (hx : x.PosSemidef) : x.PosDef ↔ IsUnit x :=
by
refine ⟨fun h => h.isUnit, fun h => ⟨hx.1, fun v hv => ?_⟩⟩
obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
simp_rw [dotProduct_mulVec, ← vecMul_vecMul, star_eq_conjTranspose, ← star_mulVec, ← dotProduct_mulVec,
dotProduct_star_self_pos_iff]
contrapose! hv
rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h), mulVecLin_apply, ← mulVec_mulVec,
hv, mulVec_zero]
