selfAdjointPart_add_skewAdjointPart

English

Elements of a star module decompose uniquely as the sum of their self-adjoint and skew-adjoint parts: x = (selfAdjointPart x) + (skewAdjointPart x).

Русский

Любой элемент звёздового модуля разлагается единственным образом в сумму своей самосопряжённой и космодружённой частей: x = (самосопряжённая часть x) + (космодружённая часть x).

LaTeX

$$$A \cong_{\text{lin}} \mathrm{selfAdjoint} A \times \mathrm{skewAdjoint} A, \quad x \mapsto (\text{selfAdjointPart}(x), \text{skewAdjointPart}(x))$$

Lean4

theorem selfAdjointPart_add_skewAdjointPart (x : A) : (selfAdjointPart R x : A) + skewAdjointPart R x = x := by
  simp only [smul_sub, selfAdjointPart_apply_coe, smul_add, skewAdjointPart_apply_coe, add_add_sub_cancel,
    invOf_two_smul_add_invOf_two_smul]

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