realPart_add_I_smul_imaginaryPart

English

The imaginary part of a self-adjoint element vanishes, i.e., Im(x) = 0 when x is self-adjoint.

Русский

Мнимая часть самосопряжённого элемента равна нулю.

LaTeX

$$$\\forall x\\in \\mathrm{selfAdjoint}(A), \\Im(x) = 0$$$

Lean4

/-- The standard decomposition of `ℜ a + Complex.I • ℑ a = a` of an element of a star module over
`ℂ` into a linear combination of self adjoint elements. -/
theorem realPart_add_I_smul_imaginaryPart (a : A) : (ℜ a : A) + I • (ℑ a : A) = a := by
  simpa only [smul_smul, realPart_apply_coe, imaginaryPart_apply_coe, neg_smul, I_mul_I, one_smul, neg_sub,
    add_add_sub_cancel, smul_sub, smul_add, neg_sub_neg, invOf_eq_inv] using invOf_two_smul_add_invOf_two_smul ℝ a

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