imaginaryPart_eq_neg_I_smul_skewAdjointPart

English

The imaginary part of a elements equals minus i times its skewAdjoint part: Im(a) = -i · skewAdjointPart(a).

Русский

Мнимая часть элемента равна -i умножению на его косо-сопряжённую часть: Im(a) = -i · skewAdjointPart(a).

LaTeX

$$$\\operatorname{imaginaryPart}(a) = -i \\cdot \\operatorname{skewAdjointPart}(a)$$$

Lean4

theorem imaginaryPart_eq_neg_I_smul_skewAdjointPart (x : A) : (imaginaryPart x : A) = -I • (skewAdjointPart ℝ x : A) :=
  rfl

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