linearEquiv_det_conjLIE

Mathlib.Analysis.Complex.OperatorNorm

URI: https://scilib.ai/kg/mathlib#Complex.linearEquiv_det_conjLIE

← MathLib Explorer

English

The determinant of conjLIE as a linear isometry equals −1.

Русский

Детерминант conjLIE как линейного изометрия равен −1.

LaTeX

$$$\\operatorname{det}(\\text{conjLIE}^{\\text{toLinearEquiv}}) = -1$$$

Lean4

/-- The determinant of `conjLIE`, as a linear equiv. -/
@[simp]
theorem linearEquiv_det_conjLIE : LinearEquiv.det conjLIE.toLinearEquiv = -1 :=
  linearEquiv_det_conjAe

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

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

Разделы

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

Аффилиация

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