inv_sqrt

Mathlib.Analysis.Matrix.Order

URI: https://scilib.ai/kg/mathlib#Matrix.PosSemidef.inv_sqrt

← MathLib Explorer

English

If A is positive semidefinite, then (sqrt A)^{-1} = sqrt(A^{-1}).

Русский

Если A положительно полуопределена, то (sqrt A)^{-1} = sqrt(A^{-1}).

LaTeX

$$$(\sqrt{A})^{-1} = \sqrt{A^{-1}}$.$$

Lean4

theorem inv_sqrt : (CFC.sqrt A)⁻¹ = CFC.sqrt A⁻¹ := by
  rw [eq_comm, CFC.sqrt_eq_iff _ _ hA.inv.nonneg (CFC.sqrt_nonneg A).posSemidef.inv.nonneg, ← sq, inv_pow',
    CFC.sq_sqrt A]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru