coe_selfAdjointPart_apply — Mathlib

English

If x is self-adjoint, then the self-adjoint part of x equals x, i.e., the map fixes self-adjoint elements pointwise.

Русский

Если x самосопряжён, то самосопряжённая часть x равна x; отображение фиксирует самосопряжённые элементы по точкам.

LaTeX

$$$\text{selfAdjointPart}(R, x) = x$ for all $x$ with $x^{*}=x$$$

Lean4

theorem coe_selfAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) : (selfAdjointPart R x : A) = x := by
  rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]

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