imaginaryPart — Mathlib

English

Multiplication by I is the inverse of multiplying by -I on the skewAdjoint-to-SelfAdjoint correspondence; i.e., Im(I a) = Re(a).

Русский

Умножение на i обратимо по отношению к умножению на -i в отображении между частями; Im(Ia) = Re(a).

LaTeX

$$$\\operatorname{imaginaryPart}(I a) = \\operatorname{realPart}(a)$$$

Lean4

nonrec theorem imaginaryPart {x : A} (hx : IsSelfAdjoint x) : ℑ x = 0 := by
  rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]

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