isUnit_sqrt_iff

Mathlib.Analysis.Matrix.Order

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

English

IsUnit(sqrt A) iff IsUnit(A) for PSD A.

Русский

IsUnit( sqrt(A) ) тогда и только тогда, когда IsUnit(A) для PSD A.

LaTeX

$$$\text{IsUnit}(\sqrt{A}) \iff \text{IsUnit}(A) \quad (A \ PosSemidef).$$$

Lean4

@[deprecated CFC.isUnit_sqrt_iff (since := "2025-09-22")]
theorem isUnit_sqrt_iff : IsUnit (CFC.sqrt A) ↔ IsUnit A :=
  CFC.isUnit_sqrt_iff A

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

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

Разделы

Аффилиация

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