skewAdjointPart_eq_I_smul_imaginaryPart

English

The real part of the skewAdjoint part equals I times the imaginary part: skewAdjointPartℝ(a) = I · ImaginaryPart(a).

Русский

Действительная часть skewAdjoint(a) равна I умноженному на мнимую часть a.

LaTeX

$$$\\operatorname{skewAdjointPart}(\\mathbb{R}\\, a) = i \\cdot \\operatorname{imaginaryPart}(a)$$$

Lean4

theorem skewAdjointPart_eq_I_smul_imaginaryPart (x : A) : (skewAdjointPart ℝ x : A) = I • (imaginaryPart x : A) := by
  simp [imaginaryPart_apply_coe, smul_smul]

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