sqrt_eq_one_iff

Mathlib.Analysis.Matrix.Order

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

English

The square root equals 1 iff the matrix equals 1 (for PSD A).

Русский

Квадратный корень равен единице тогда и только тогда, когда матрица равна единице (в контексте PSD).

LaTeX

$$$\sqrt{A} = 1 \iff A = 1$ (при A \ PosSemidef).$$

Lean4

@[deprecated CFC.sqrt_eq_one_iff (since := "2025-09-23")]
theorem sqrt_eq_one_iff : CFC.sqrt A = 1 ↔ A = 1 :=
  CFC.sqrt_eq_one_iff A

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

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

Разделы

Аффилиация

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