imaginaryPart_apply_coe — Mathlib

English

The real part of a self-adjoint element (viewed in A) equals the element itself.

Русский

Действительная часть самосопряжённого элемента совпадает с самим элементом.

LaTeX

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

Lean4

theorem imaginaryPart_apply_coe (a : A) : (ℑ a : A) = -I • (2 : ℝ)⁻¹ • (a - star a) :=
  by
  unfold imaginaryPart
  simp only [LinearMap.coe_comp, Function.comp_apply, skewAdjoint.negISMul_apply_coe, skewAdjointPart_apply_coe,
    invOf_eq_inv, neg_smul]

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