det_conjAe

Mathlib.LinearAlgebra.Complex.Determinant

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

← MathLib Explorer

English

The determinant of the linear map conjAe (conjugation by the unitary element a) equals -1.

Русский

Определитель линейного отображения conjAe равен -1.

LaTeX

$$det conjAe.toLinearMap = -1.$$

Lean4

/-- The determinant of `conjAe`, as a linear map. -/
@[simp]
theorem det_conjAe : LinearMap.det conjAe.toLinearMap = -1 :=
  by
  rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]
  simp

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

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

Разделы

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

Аффилиация

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